---

Step * of Lemma pi12-sqle-spread

∀[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 Unfold `pi1` 0
   THEN (InstLemma `lifting-strict-spread`  [⌜so_lambda(x,y,z,w.P[x;y])⌝;⌜snd(t)⌝;⌜⋅⌝;⌜⋅⌝;⌜t⌝;⌜λ2x y.x⌝]⋅ THENA Auto)
   THEN HypSubst' (-1) 0
   THEN SqReasoning) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  Unfold  `pi1`  0
  THEN  (InstLemma  `lifting-strict-spread` 
              [\mkleeneopen{}so\_lambda(x,y,z,w.P[x;y])\mkleeneclose{};\mkleeneopen{}snd(t)\mkleeneclose{};\mkleeneopen{}\mcdot{}\mkleeneclose{};\mkleeneopen{}\mcdot{}\mkleeneclose{};\mkleeneopen{}t\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x  y.x\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  HypSubst'  (-1)  0
  THEN  SqReasoning)

---

Home Index