---

Step * 1 2 2 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])
⊢ ∀x,y:T2.  {r2[x;y] ⇐ r1[x;y]}
BY
{ (((Unfold `guard` 0 THENM UnivCD) THENM BackThruHyp 6) THEN 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{}  \mforall{}x,y:T2.    \{r2[x;y]  \mLeftarrow{}{}  r1[x;y]\}


By

---

Latex:
(((Unfold  `guard`  0  THENM  UnivCD)  THENM  BackThruHyp  6)  THEN  Auto)

---

Home Index