Step
*
of Lemma
sq_stable__trans
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ((∀x,y:T. SqStable(R[x;y]))
⇒ SqStable(Trans(T;y,x.R[x;y])))
BY
{ (Unfold `trans` 0 THEN Auto) }
Latex:
Latex:
\mforall{}[T:Type]. \mforall{}[R:T {}\mrightarrow{} T {}\mrightarrow{} \mBbbP{}]. ((\mforall{}x,y:T. SqStable(R[x;y])) {}\mRightarrow{} SqStable(Trans(T;y,x.R[x;y])))
By
Latex:
(Unfold `trans` 0 THEN Auto)
Home
Index