---

Step * of Lemma spread-sq-pi12

∀[t:Top]. ∀[P:Base].  P[fst(t);snd(t)] ~ let x,y = t in P[x;y] supposing strict4(λx,y,z,w. P[x;y])
BY
{ (Auto⋅ THEN SqequalSqle THEN (BLemma `spread-sqle-pi12` ORELSE BLemma `pi12-sqle-spread`) THEN Auto) }

1
1. t : Top
2. P : Base
3. strict4(λx,y,z,w. P[x;y])
4. u : Base@i
5. v : Base@i
⊢ P[exception(u; v);exception(u; v)] ~ exception(u; v)

---

Latex:

---

Latex:
\mforall{}[t:Top].  \mforall{}[P:Base].    P[fst(t);snd(t)]  \msim{}  let  x,y  =  t  in  P[x;y]  supposing  strict4(\mlambda{}x,y,z,w.  P[x;y])


By

---

Latex:
(Auto\mcdot{}  THEN  SqequalSqle  THEN  (BLemma  `spread-sqle-pi12`  ORELSE  BLemma  `pi12-sqle-spread`)  THEN  Auto)

---

Home Index