---

Step * of Lemma lifting-strict-spread

∀[F:Base]. ∀[p,q,r:Top].
  ∀[a,B:Top].  (F[let x,y = a in B[x;y];p;q;r] ~ let x,y = a in F[B[x;y];p;q;r]) supposing strict4(λx,y,z,w. F[x;y;z;w])
BY
{ (SqReasoning THEN (GenConcl ⌜a = zzz ∈ (Top × Top)⌝⋅ THENA Auto) THEN D -2 THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[F:Base].  \mforall{}[p,q,r:Top].
    \mforall{}[a,B:Top].    (F[let  x,y  =  a  in  B[x;y];p;q;r]  \msim{}  let  x,y  =  a  in  F[B[x;y];p;q;r]) 
    supposing  strict4(\mlambda{}x,y,z,w.  F[x;y;z;w])


By

---

Latex:
(SqReasoning  THEN  (GenConcl  \mkleeneopen{}a  =  zzz\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  D  -2  THEN  Reduce  0  THEN  Auto)

---

Home Index