Step
*
of Lemma
monotone-incr-chain
∀F:Type ⟶ Type. (Monotone(T.F T)
⇒ (λn.(F^n Void) ∈ type-incr-chain{i:l}()))
BY
{ (Auto THEN MemTypeCD THEN Reduce 0 THEN Auto) }
Latex:
Latex:
\mforall{}F:Type {}\mrightarrow{} Type. (Monotone(T.F T) {}\mRightarrow{} (\mlambda{}n.(F\^{}n Void) \mmember{} type-incr-chain\{i:l\}()))
By
Latex:
(Auto THEN MemTypeCD THEN Reduce 0 THEN Auto)
Home
Index