---

Step * of Lemma test-spread-normalize

∀[a,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
{ (UnivCD THENA Auto) }

1
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>]

---

Latex:

---

Latex:
\mforall{}[a,B:Top].    (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:
(UnivCD  THENA  Auto)

---

Home Index