---

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


1. as : Base
2. ff ~ tt
3. 0 ≤ 0
4. (as)↓
5. ∀a,b:Base.  (if as = Ax then a otherwise b ~ b)
6. as ~ <fst(as), snd(as)>
⊢ as = [] ∈ Base
BY
{ InstLemma `not-btrue-sqeq-bfalse` [] }

1
1. as : Base
2. ff ~ tt
3. 0 ≤ 0
4. (as)↓
5. ∀a,b:Base.  (if as = Ax then a otherwise b ~ b)
6. as ~ <fst(as), snd(as)>
7. ¬(ff ~ tt)
⊢ as = [] ∈ Base

---

Latex:

---

Latex:

1.  as  :  Base
2.  ff  \msim{}  tt
3.  0  \mleq{}  0
4.  (as)\mdownarrow{}
5.  \mforall{}a,b:Base.    (if  as  =  Ax  then  a  otherwise  b  \msim{}  b)
6.  as  \msim{}  <fst(as),  snd(as)>
\mvdash{}  as  =  []


By

---

Latex:
InstLemma  `not-btrue-sqeq-bfalse`  []

---

Home Index