---

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


1. as : Base
2. if as is a pair then ff otherwise ⊥ ~ tt
3. (if as is a pair then ff otherwise ⊥)↓
4. (as)↓
5. ∀a,b:Base.  (if as = Ax then a otherwise b ~ b)
⊢ as = [] ∈ Base
BY
{ (FLemma `has-value-implies-dec-ispair-2` [-2] THENA Auto)⋅ }

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

---

Latex:

---

Latex:

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


By

---

Latex:
(FLemma  `has-value-implies-dec-ispair-2`  [-2]  THENA  Auto)\mcdot{}

---

Home Index