Step
*
1
of Lemma
lifting-ispair-concat
1. c : Base
2. b : Base
3. a : Base
4. (concat(if a is a pair then b otherwise c))↓
⊢ concat(if a is a pair then b otherwise c) ≤ if a is a pair then concat(b) otherwise concat(c)
BY
{ ((FLemma `concat-strict` [-1] THENA Auto) THEN HasValueD (-1) THEN (HVimplies 0 [2] THEN HVimplies 0 [1;1])⋅) }
Latex:
Latex:
1. c : Base
2. b : Base
3. a : Base
4. (concat(if a is a pair then b otherwise c))\mdownarrow{}
\mvdash{} concat(if a is a pair then b otherwise c) \mleq{} if a is a pair then concat(b) otherwise concat(c)
By
Latex:
((FLemma `concat-strict` [-1] THENA Auto)
THEN HasValueD (-1)
THEN (HVimplies 0 [2] THEN HVimplies 0 [1;1])\mcdot{})
Home
Index