Step
*
of Lemma
sq_stable__inverse
∀[T:Type]. ∀[op:T ⟶ T ⟶ T]. ∀[id:T]. ∀[inv:T ⟶ T]. SqStable(Inverse(T;op;id;inv))
BY
{ Unfold `inverse` 0 THENM UnivCD
THENM ProveSqStable THENA Auto }
Latex:
Latex:
\mforall{}[T:Type]. \mforall{}[op:T {}\mrightarrow{} T {}\mrightarrow{} T]. \mforall{}[id:T]. \mforall{}[inv:T {}\mrightarrow{} T]. SqStable(Inverse(T;op;id;inv))
By
Latex:
Unfold `inverse` 0 THENM UnivCD
THENM ProveSqStable THENA Auto
Home
Index