---

Step * of Lemma assert-null-base

∀[as:Base]. uiff(null(as) ~ tt;as ~ [])
BY
{ (Auto
   THEN Try (Complete ((HypSubst (-1) 0 THEN SymbComp 0 THEN Auto)))
   THEN (Assert (null(as))↓ BY
               (HypSubst' (-1)0 THEN Auto))
   THEN Unfold `null` -1
   THEN HasValueD (-1)) }

1
1. as : Base
2. null(as) ~ tt
3. (if as is a pair then ff otherwise if as = Ax then tt otherwise ⊥)↓
4. (as)↓
⊢ as = [] ∈ Base

---

Latex:

---

Latex:
\mforall{}[as:Base].  uiff(null(as)  \msim{}  tt;as  \msim{}  [])


By

---

Latex:
(Auto
  THEN  Try  (Complete  ((HypSubst  (-1)  0  THEN  SymbComp  0  THEN  Auto)))
  THEN  (Assert  (null(as))\mdownarrow{}  BY
                          (HypSubst'  (-1)0  THEN  Auto))
  THEN  Unfold  `null`  -1
  THEN  HasValueD  (-1))

---

Home Index