Step
*
of Lemma
cbv_bottom_lemma
∀X:Top. (eval x = ⊥ in X[x] ~ ⊥)
BY
{ SqReasoning }
Latex:
Latex:
\mforall{}X:Top.  (eval  x  =  \mbot{}  in  X[x]  \msim{}  \mbot{})
By
Latex:
SqReasoning
Home
Index