---

Step * of Lemma lifting-strict-decide

∀[F:Base]. ∀[p,q,r:Top].
  ∀[a,A,B:Top].
    (F[case a of inl(x) => A[x] | inr(x) => B[x];p;q;r] ~ case a of inl(x) => F[A[x];p;q;r] | inr(x) => F[B[x];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,A,B:Top].
        (F[case  a  of  inl(x)  =>  A[x]  |  inr(x)  =>  B[x];p;q;r]  \msim{}  case  a
          of  inl(x)  =>
          F[A[x];p;q;r]
          |  inr(x)  =>
          F[B[x];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