---

Step * of Lemma lifting-isaxiom-concat

∀[a,b,c:Top].  (concat(if a = Ax then b otherwise c) ~ if a = Ax then concat(b) otherwise concat(c))
BY
{ ((UnivCD THENA Auto)
   THEN InstLemma `lifting-strict-isaxiom`
   [⌜so_lambda(x,y,z,w.concat(x))⌝;⌜⋅⌝;⌜⋅⌝;⌜⋅⌝]⋅
   THEN Auto
   THEN ProveStrict) }

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  InstLemma  `lifting-strict-isaxiom`
  [\mkleeneopen{}so\_lambda(x,y,z,w.concat(x))\mkleeneclose{};\mkleeneopen{}\mcdot{}\mkleeneclose{};\mkleeneopen{}\mcdot{}\mkleeneclose{};\mkleeneopen{}\mcdot{}\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  ProveStrict)

---

Home Index