---

Step * 1 of Lemma test-spread-normalize


1. a : Top
2. B : Top
⊢ let x,y = a 
  in if a is a pair then B[a] otherwise 2 ~ let x,y = a 
                                            in B[<x, y>]
BY
{ (NormalizeSpread 0 THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  Top
2.  B  :  Top
\mvdash{}  let  x,y  =  a 
    in  if  a  is  a  pair  then  B[a]  otherwise  2  \msim{}  let  x,y  =  a 
                                                                                        in  B[<x,  y>]


By

---

Latex:
(NormalizeSpread  0  THEN  Reduce  0  THEN  Auto)

---

Home Index