---

Step * 1 1 of Lemma wellfounded_functionality_wrt_implies

.....equality..... 
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])
7. ∀[P:T1 ⟶ ℙ]. ((∀j:T1. ((∀k:T1. (r1[k;j] ⇒ P[k])) ⇒ P[j])) ⇒ {∀n:T1. P[n]})
8. P : T2 ⟶ ℙ
9. ∀j:T2. ((∀k:T2. (r2[k;j] ⇒ P[k])) ⇒ P[j])
⊢ (∀n:T2. P[n]) = (∀n:T1. P[n]) ∈ ℙ{[1 | i 0]}
BY
{ (Repeat EqCD THEN Auto) }

---

Latex:

---

Latex:
.....equality..... 
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{}{}  r2[x;y])
7.  \mforall{}[P:T1  {}\mrightarrow{}  \mBbbP{}].  ((\mforall{}j:T1.  ((\mforall{}k:T1.  (r1[k;j]  {}\mRightarrow{}  P[k]))  {}\mRightarrow{}  P[j]))  {}\mRightarrow{}  \{\mforall{}n:T1.  P[n]\})
8.  P  :  T2  {}\mrightarrow{}  \mBbbP{}
9.  \mforall{}j:T2.  ((\mforall{}k:T2.  (r2[k;j]  {}\mRightarrow{}  P[k]))  {}\mRightarrow{}  P[j])
\mvdash{}  (\mforall{}n:T2.  P[n])  =  (\mforall{}n:T1.  P[n])


By

---

Latex:
(Repeat  EqCD  THEN  Auto)

---

Home Index