---

Step * of Lemma co-cons-not-co-nil

∀[T:Type]. ∀[a:T]. ∀[b:colist(T)].  uiff([a / b] = () ∈ colist(T);False)
BY
{ (Auto THEN (ApFunToHypEquands `Z' ⌜null(Z)⌝ ⌜𝔹⌝  (-1)⋅ THENA (colistD (-1) THEN Reduce 0 THEN Auto))) }

1
1. T : Type
2. a : T
3. b : colist(T)
4. [a / b] = () ∈ colist(T)
5. null([a / b]) = null(())
⊢ False

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[a:T].  \mforall{}[b:colist(T)].    uiff([a  /  b]  =  ();False)


By

---

Latex:
(Auto
  THEN  (ApFunToHypEquands  `Z'  \mkleeneopen{}null(Z)\mkleeneclose{}  \mkleeneopen{}\mBbbB{}\mkleeneclose{}    (-1)\mcdot{}  THENA  (colistD  (-1)  THEN  Reduce  0  THEN  Auto))
  )

---

Home Index