---

Step * 1 of Lemma sq_stable__ident


1. T : Type
2. op : T ⟶ T ⟶ T
3. id : T
⊢ SqStable(∀[x:T]. (((x op id) = x ∈ T) ∧ ((id op x) = x ∈ T)))
BY
{ ProveSqStable THEN Auto }

---

Latex:

---

Latex:

1.  T  :  Type
2.  op  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  T
3.  id  :  T
\mvdash{}  SqStable(\mforall{}[x:T].  (((x  op  id)  =  x)  \mwedge{}  ((id  op  x)  =  x)))


By

---

Latex:
ProveSqStable  THEN  Auto

---

Home Index