---

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

∀[t:Base]. (if ispair(t) then t ~ <fst(t), snd(t)> else t ~ Ax fi ) supposing ((t)↓ and is-list-if-has-value-rec(t))
BY
{ (Auto
   THEN Try (Complete ((BLemma `ispair-bool-if-has-value` THEN Auto)))
   THEN RepUR ``is-list-if-has-value-rec is-list-if-has-value-fun`` (-2)
   THEN (With ⌜1⌝ (D (-2))⋅ THENA Auto)
   THEN Reduce (-1)
   THEN (D (-1) THENA Auto)
   THEN HVimplies2 0 [1]) }

1
1. t : Base
2. (t)↓
3. ↑isaxiom(t)
4. ∀a,b:Top.  (if t is a pair then a otherwise b ~ b)
⊢ t ~ Ax

---

Latex:

---

Latex:
\mforall{}[t:Base]
    (if  ispair(t)  then  t  \msim{}  <fst(t),  snd(t)>  else  t  \msim{}  Ax  fi  )  supposing 
          ((t)\mdownarrow{}  and 
          is-list-if-has-value-rec(t))


By

---

Latex:
(Auto
  THEN  Try  (Complete  ((BLemma  `ispair-bool-if-has-value`  THEN  Auto)))
  THEN  RepUR  ``is-list-if-has-value-rec  is-list-if-has-value-fun``  (-2)
  THEN  (With  \mkleeneopen{}1\mkleeneclose{}  (D  (-2))\mcdot{}  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  (D  (-1)  THENA  Auto)
  THEN  HVimplies2  0  [1])

---

Home Index