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