---

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