---

Step * 1 1 of Lemma equipollent-identity

.....subterm..... T:t
1:n
1. A : Type
2. B : Type
3. B ~ Unit@i
4. a3 : B@i
5. a4 : A@i
6. a5 : B@i
7. a6 : A@i
8. a4 = a6 ∈ A@i
⊢ a3 = a5 ∈ B
BY
{ ((D 3 THEN D 4 THEN BackThruHyp' 4) THEN Auto) }

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  A  :  Type
2.  B  :  Type
3.  B  \msim{}  Unit@i
4.  a3  :  B@i
5.  a4  :  A@i
6.  a5  :  B@i
7.  a6  :  A@i
8.  a4  =  a6@i
\mvdash{}  a3  =  a5


By

---

Latex:
((D  3  THEN  D  4  THEN  BackThruHyp'  4)  THEN  Auto)

---

Home Index