---

Step * of Lemma spread-decide

∀[x,d,F,G:Top].
  (let a,b = x 
   in case d[a;b] of inl(u) => F[a;b;u] | inr(u) => G[a;b;u] ~ case let a,b = x 
                                                                    in d[a;b]
   of inl(u) =>
   let a,b = x 
   in F[a;b;u]
   | inr(u) =>
   let a,b = x 
   in G[a;b;u])
BY
{ ((UnivCD THENA Auto) THEN RW (AddrC [2] (LiftC true)) 0 THEN SqReasoning) }

---

Latex:

---

Latex:
\mforall{}[x,d,F,G:Top].
    (let  a,b  =  x 
      in  case  d[a;b]  of  inl(u)  =>  F[a;b;u]  |  inr(u)  =>  G[a;b;u]  \msim{}  case  let  a,b  =  x 
                                                                                                                                        in  d[a;b]
      of  inl(u)  =>
      let  a,b  =  x 
      in  F[a;b;u]
      |  inr(u)  =>
      let  a,b  =  x 
      in  G[a;b;u])


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RW  (AddrC  [2]  (LiftC  true))  0  THEN  SqReasoning)

---

Home Index