Step 
*
 of Lemma 
normalization-spread3
∀[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