---

Step * of Lemma sq_stable__bilinear

∀[T:Type]. ∀[pl,tm:T ⟶ T ⟶ T].  SqStable(BiLinear(T;pl;tm))
BY
{ Unfold `bilinear` 0 THEN UnivCD 
THENM ProveSqStable THEN Auto }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[pl,tm:T  {}\mrightarrow{}  T  {}\mrightarrow{}  T].    SqStable(BiLinear(T;pl;tm))


By

---

Latex:
Unfold  `bilinear`  0  THEN  UnivCD 
THENM  ProveSqStable  THEN  Auto

---

Home Index