---

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