Step
*
of Lemma
funtype-auto-test-case
∀m:ℕ. ∀A:ℕm ⟶ Type. ∀x:⋂x:Type. (x ⟶ x). ∀T:Type. (x ∈ funtype(0;A;T) ⟶ T)
BY
{ (skip{Auto used to loop by backchaining thru ⋂x:Type. (x ⟶ x) which is the same as ∀[x:ℙ]. (x
⇒ x) ⋅} THEN Auto) }
Latex:
Latex:
\mforall{}m:\mBbbN{}. \mforall{}A:\mBbbN{}m {}\mrightarrow{} Type. \mforall{}x:\mcap{}x:Type. (x {}\mrightarrow{} x). \mforall{}T:Type. (x \mmember{} funtype(0;A;T) {}\mrightarrow{} T)
By
Latex:
(skip\{Auto used to loop by backchaining thru \mcap{}x:Type. (x {}\mrightarrow{} x)
which is the same as \mforall{}[x:\mBbbP{}]. (x {}\mRightarrow{} x) \mcdot{}\}
THEN Auto
)
Home
Index