---

Step * of Lemma equality-test

∀[A,B,C:Type].  ((A = B ∈ Type) ⇒ (C = B ∈ Type) ⇒ (∀[x,y,z:A].  ((x = y ∈ A) ⇒ (z = y ∈ A) ⇒ (x = z ∈ C))))
BY
{ TACTIC:Intros }

1
1. A : Type
2. B : Type
3. C : Type
4. A = B ∈ Type
5. C = B ∈ Type
6. x : A
7. y : A
8. z : A
9. x = y ∈ A
10. z = y ∈ A
⊢ x = z ∈ C

---

Latex:

---

Latex:
\mforall{}[A,B,C:Type].    ((A  =  B)  {}\mRightarrow{}  (C  =  B)  {}\mRightarrow{}  (\mforall{}[x,y,z:A].    ((x  =  y)  {}\mRightarrow{}  (z  =  y)  {}\mRightarrow{}  (x  =  z))))


By

---

Latex:
TACTIC:Intros

---

Home Index