---

Step * 1 of Lemma bigrel-induction-monotone


1. 0 + 1 ≠ 0
2. [T] : Type
3. P : (T ⟶ T ⟶ ℙ) ⟶ ℙ
4. F : (T ⟶ T ⟶ ℙ) ⟶ T ⟶ T ⟶ ℙ
5. rel-monotone{i:l}(T;R.F[R])
6. ∀Rs:ℕ ⟶ T ⟶ T ⟶ ℙ. ((∀n:ℕ. Rs[n + 1] => Rs[n]) ⇒ (∀n:ℕ. P[Rs[n]]) ⇒ P[isect-rel(ℕ;n.Rs[n])])
7. ∀R:T ⟶ T ⟶ ℙ. (P[R] ⇒ P[F[R]])
8. P[λx,y. True]
⊢ F[λx,y. True] => λx,y. True
BY
{ (RepUR ``rel_implies`` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  0  +  1  \mneq{}  0
2.  [T]  :  Type
3.  P  :  (T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{})  {}\mrightarrow{}  \mBbbP{}
4.  F  :  (T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{})  {}\mrightarrow{}  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
5.  rel-monotone\{i:l\}(T;R.F[R])
6.  \mforall{}Rs:\mBbbN{}  {}\mrightarrow{}  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}.  ((\mforall{}n:\mBbbN{}.  Rs[n  +  1]  =>  Rs[n])  {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  P[Rs[n]])  {}\mRightarrow{}  P[isect-rel(\mBbbN{};n.Rs[n])])
7.  \mforall{}R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}.  (P[R]  {}\mRightarrow{}  P[F[R]])
8.  P[\mlambda{}x,y.  True]
\mvdash{}  F[\mlambda{}x,y.  True]  =>  \mlambda{}x,y.  True


By

---

Latex:
(RepUR  ``rel\_implies``  0  THEN  Auto)

---

Home Index