---

Step * of Lemma lifting-strict-isatom2

∀[F:Base]. ∀[p,q,r:Top].
  ∀[a,b,c:Top].  (F[isatom2(a;b;c);p;q;r] ~ isatom2(a;F[b;p;q;r];F[c;p;q;r])) supposing strict4(λx,y,z,w. F[x;y;z;w])
BY
{ SqReasoning }

---

Latex:

---

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


By

---

Latex:
SqReasoning

---

Home Index