---

Step * 1 1 1 of Lemma assert-null-base


1. as : Base
2. null(as) ~ tt
3. (if as is a pair then ff otherwise if as = Ax then tt otherwise ⊥)↓
4. (as)↓
5. as ~ Ax
⊢ as = [] ∈ Base
BY
{ (HypSubst (-1) 0 THEN SymbComp 0 THEN Auto) }

---

Latex:

---

Latex:

1.  as  :  Base
2.  null(as)  \msim{}  tt
3.  (if  as  is  a  pair  then  ff  otherwise  if  as  =  Ax  then  tt  otherwise  \mbot{})\mdownarrow{}
4.  (as)\mdownarrow{}
5.  as  \msim{}  Ax
\mvdash{}  as  =  []


By

---

Latex:
(HypSubst  (-1)  0  THEN  SymbComp  0  THEN  Auto)

---

Home Index