---

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


1. t : Base
2. (t)↓
3. ↑isaxiom(t)
4. ∀a,b:Top.  (if t is a pair then a otherwise b ~ b)
⊢ t ~ Ax
BY
{ xxx((Assert ⌜isaxiom(t) ∈ 𝔹⌝⋅ THENA HVimplies2 0 [2])
      THEN BoolCase ⌜isaxiom(t)⌝⋅
      THEN Auto
      THEN FLemma `isaxiom-implies` [-1]
      THEN Auto)xxx }

---

Latex:

---

Latex:

1.  t  :  Base
2.  (t)\mdownarrow{}
3.  \muparrow{}isaxiom(t)
4.  \mforall{}a,b:Top.    (if  t  is  a  pair  then  a  otherwise  b  \msim{}  b)
\mvdash{}  t  \msim{}  Ax


By

---

Latex:
xxx((Assert  \mkleeneopen{}isaxiom(t)  \mmember{}  \mBbbB{}\mkleeneclose{}\mcdot{}  THENA  HVimplies2  0  [2])
        THEN  BoolCase  \mkleeneopen{}isaxiom(t)\mkleeneclose{}\mcdot{}
        THEN  Auto
        THEN  FLemma  `isaxiom-implies`  [-1]
        THEN  Auto)xxx

---

Home Index