---

Step * of Lemma lifting-ispair-concat

∀[a,b,c:Top].  (concat(if a is a pair then b otherwise c) ~ if a is a pair then concat(b) otherwise concat(c))
BY
{ SqReasoning }

1
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)

---

Latex:

---

Latex:
\mforall{}[a,b,c:Top].
    (concat(if  a  is  a  pair  then  b  otherwise  c)  \msim{}  if  a  is  a  pair  then  concat(b)  otherwise  concat(c))


By

---

Latex:
SqReasoning

---

Home Index