---

Step * 1 1 of Lemma implies-bigrel


1. [T] : Type
2. F : (T ⟶ T ⟶ ℙ) ⟶ T ⟶ T ⟶ ℙ
3. rel-monotone{i:l}(T;R.F[R])
4. R' : T ⟶ T ⟶ ℙ
5. R' => F[R']
6. 0 < 1
⊢ R' => λx,y. True
BY
{ (D 0 THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  F  :  (T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{})  {}\mrightarrow{}  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  rel-monotone\{i:l\}(T;R.F[R])
4.  R'  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
5.  R'  =>  F[R']
6.  0  <  1
\mvdash{}  R'  =>  \mlambda{}x,y.  True


By

---

Latex:
(D  0  THEN  Reduce  0  THEN  Auto)

---

Home Index