Step
*
of Lemma
t-sqle-subtype
∀[A,B:Type]. ∀[a,b:A]. (t-sqle(A;a;b)
⇒ t-sqle(B;a;b)) supposing A ⊆r B
BY
{ (Auto THEN RepeatFor 4 (ParallelLast)) }
Latex:
Latex:
\mforall{}[A,B:Type]. \mforall{}[a,b:A]. (t-sqle(A;a;b) {}\mRightarrow{} t-sqle(B;a;b)) supposing A \msubseteq{}r B
By
Latex:
(Auto THEN RepeatFor 4 (ParallelLast))
Home
Index