---

Step * of Lemma simplify-equal-imp

∀[T:Type]. ∀[x,y,z:T].  uiff(x = z ∈ T supposing x = y ∈ T;¬(x = y ∈ T)) supposing ¬(y = z ∈ T)
BY
{ xxx(Auto THEN (ParallelOp (-2)) THEN ThinTrivial THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[x,y,z:T].    uiff(x  =  z  supposing  x  =  y;\mneg{}(x  =  y))  supposing  \mneg{}(y  =  z)


By

---

Latex:
xxx(Auto  THEN  (ParallelOp  (-2))  THEN  ThinTrivial  THEN  Auto)xxx

---

Home Index