---

Step * 1 2 1 of Lemma wellfounded_functionality_wrt_iff


1. T1 : Type
2. T2 : Type
3. r1 : T1 ⟶ T1 ⟶ ℙ
4. r2 : T2 ⟶ T2 ⟶ ℙ
5. T1 = T2 ∈ Type
6. ∀x,y:T1.  (r1[x;y] ⇐⇒ r2[x;y])
⊢ T2 = T1 ∈ Type
BY
{ Auto }

---

Latex:

---

Latex:

1.  T1  :  Type
2.  T2  :  Type
3.  r1  :  T1  {}\mrightarrow{}  T1  {}\mrightarrow{}  \mBbbP{}
4.  r2  :  T2  {}\mrightarrow{}  T2  {}\mrightarrow{}  \mBbbP{}
5.  T1  =  T2
6.  \mforall{}x,y:T1.    (r1[x;y]  \mLeftarrow{}{}\mRightarrow{}  r2[x;y])
\mvdash{}  T2  =  T1


By

---

Latex:
Auto

---

Home Index