---

Step * of Lemma name_eq_spread

∀[x,y,F:Top].  (name_eq(let a,b = x in F[a;b];y) ~ let a,b = x in name_eq(F[a;b];y))
BY
{ ((UnivCD THENA Auto)
   THEN RepUR ``name_eq name-deq list-deq eq_atom list_ind band bfalse btrue ifthenelse it so_apply`` 0
   THEN LiftAll 0
   THEN Reduce 0
   THEN UnrollLoopsOnce) }

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  ...
  THEN  LiftAll  0
  THEN  Reduce  0
  THEN  UnrollLoopsOnce)

---

Home Index