---

Step * 1 of Lemma sq_stable__eqfun_p


1. T : Type
2. eq : T ⟶ T ⟶ 𝔹
⊢ SqStable(∀[x,y:T].  uiff(↑(x eq y);x = y ∈ T))
BY
{ ((D 0 THENA Auto) THEN D -1 THEN UnhideUsingWitness THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}
\mvdash{}  SqStable(\mforall{}[x,y:T].    uiff(\muparrow{}(x  eq  y);x  =  y))


By

---

Latex:
((D  0  THENA  Auto)  THEN  D  -1  THEN  UnhideUsingWitness  THEN  Auto)

---

Home Index