---

Step * of Lemma apply-spread

∀[p,a,F:Top].  (let x,y = p in F[x;y] a ~ let x,y = p in F[x;y] a)
BY
{ (SqReasoning
   THEN (Assert ⌜(let x,y = p in F[x;y])↓⌝⋅ THENA (RWO "-1" 0 THEN Reduce 0 THEN Auto))
   THEN (HasValueD (-1) THEN SqReasoningInstEta (-1) THEN Reduce 0 THEN Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}[p,a,F:Top].    (let  x,y  =  p  in  F[x;y]  a  \msim{}  let  x,y  =  p  in  F[x;y]  a)


By

---

Latex:
(SqReasoning
  THEN  (Assert  \mkleeneopen{}(let  x,y  =  p  in  F[x;y])\mdownarrow{}\mkleeneclose{}\mcdot{}  THENA  (RWO  "-1"  0  THEN  Reduce  0  THEN  Auto))
  THEN  (HasValueD  (-1)  THEN  SqReasoningInstEta  (-1)  THEN  Reduce  0  THEN  Auto)\mcdot{})

---

Home Index