---

Step * of Lemma is-list-if-has-value-decomp

∀t:ListLike
  ((t)↓
  ⇒ (((↑isaxiom(t)) ∧ (t = Ax ∈ Unit)) ∨ ((↑ispair(t)) ∧ (∃a:Top. ∃b:ListLike. (t = <a, b> ∈ (Top × ListLike))))))
BY
{ (Intro THEN (D 0 THENA (At ⌜Type⌝ (D 0)⋅ THEN BLemma `is-list-if-has-value-hv-prp` THEN Auto))) }

1
1. t : ListLike
2. (t)↓
⊢ ((↑isaxiom(t)) ∧ (t = Ax ∈ Unit)) ∨ ((↑ispair(t)) ∧ (∃a:Top. ∃b:ListLike. (t = <a, b> ∈ (Top × ListLike))))

---

Latex:

---

Latex:
\mforall{}t:ListLike
    ((t)\mdownarrow{}  {}\mRightarrow{}  (((\muparrow{}isaxiom(t))  \mwedge{}  (t  =  Ax))  \mvee{}  ((\muparrow{}ispair(t))  \mwedge{}  (\mexists{}a:Top.  \mexists{}b:ListLike.  (t  =  <a,  b>)))))


By

---

Latex:
(Intro  THEN  (D  0  THENA  (At  \mkleeneopen{}Type\mkleeneclose{}  (D  0)\mcdot{}  THEN  BLemma  `is-list-if-has-value-hv-prp`  THEN  Auto)))

---

Home Index