---

Step * of Lemma lifting-add-spread-2

∀[a:ℤ]. ∀[b,C:Top].  a + let x,y = b in C[x;y] ~ let x,y = b in a + C[x;y] supposing (a)↓
BY
{ (UnivCD THENA Auto⋅
   THEN SqReasoning
   THEN Try (((GenConcl ⌜b = zzz ∈ (Top × Top)⌝⋅ THENA Auto) THEN D -2 THEN Reduce 0 THEN Auto))
   THEN ExceptionSqequal (-1)
   THEN HypSubst' (-1) 0 
   THEN (Reduce 0 THEN Auto)
   THEN RWO "int-add-exception" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[a:\mBbbZ{}].  \mforall{}[b,C:Top].    a  +  let  x,y  =  b  in  C[x;y]  \msim{}  let  x,y  =  b  in  a  +  C[x;y]  supposing  (a)\mdownarrow{}


By

---

Latex:
(UnivCD  THENA  Auto\mcdot{}
  THEN  SqReasoning
  THEN  Try  (((GenConcl  \mkleeneopen{}b  =  zzz\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  D  -2  THEN  Reduce  0  THEN  Auto))
  THEN  ExceptionSqequal  (-1)
  THEN  HypSubst'  (-1)  0 
  THEN  (Reduce  0  THEN  Auto)
  THEN  RWO  "int-add-exception"  0
  THEN  Auto)

---

Home Index