Step
*
of Lemma
normalization-spread4
∀[p,F:Top].  (let a,b = p in F a b p ~ let a,b = p in F a b <a, b>)
BY
{ SqReasoning }
Latex:
Latex:
\mforall{}[p,F:Top].    (let  a,b  =  p  in  F  a  b  p  \msim{}  let  a,b  =  p  in  F  a  b  <a,  b>)
By
Latex:
SqReasoning
Home
Index