Step * of Lemma sq_stable__bilinear

[T:Type]. ∀[pl,tm:T ⟶ T ⟶ T].  SqStable(BiLinear(T;pl;tm))
BY
Unfold `bilinear` 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