Step
*
1
1
2
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. ∀a,b:Base. (if as = Ax then a otherwise b ~ b)
⊢ as = [] ∈ Base
BY
{ (Unfold `null` 2 THEN (RWO "-1" 2 THENA Auto) THEN (RWO "-1" 3 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)
⊢ as = [] ∈ Base
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. \mforall{}a,b:Base. (if as = Ax then a otherwise b \msim{} b)
\mvdash{} as = []
By
Latex:
(Unfold `null` 2 THEN (RWO "-1" 2 THENA Auto) THEN (RWO "-1" 3 THENA Auto)\mcdot{})
Home
Index