---

Step * of Lemma lifting-null-spread

∀[p,F:Top].  (null(let x,y = p in F[x;y]) ~ let x,y = p in null(F[x;y]))
BY
{ ((UnivCD THENA Auto)
   THEN InstLemma `lifting-strict-spread`
   [⌜so_lambda(x,y,z,w.null(x))⌝;⌜⋅⌝;⌜⋅⌝;⌜⋅⌝;⌜p⌝;⌜F⌝]⋅
   THEN Auto
   THEN ProveStrict) }

---

Latex:

---

Latex:
\mforall{}[p,F:Top].    (null(let  x,y  =  p  in  F[x;y])  \msim{}  let  x,y  =  p  in  null(F[x;y]))


By

---

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

---

Home Index