Step
*
of Lemma
evalall-inr
∀[x:Top]. (evalall(inr x ) ~ eval y = evalall(x) in inr y )
BY
{ (Auto
THEN RW (AddrC [1] (RecUnfoldC `evalall`)) 0
THEN RW (AddrC [1] (TagC (mk_tag_term 3))) 0
THEN Reduce 0
THEN Auto) }
Latex:
Latex:
\mforall{}[x:Top]. (evalall(inr x ) \msim{} eval y = evalall(x) in inr y )
By
Latex:
(Auto
THEN RW (AddrC [1] (RecUnfoldC `evalall`)) 0
THEN RW (AddrC [1] (TagC (mk\_tag\_term 3))) 0
THEN Reduce 0
THEN Auto)
Home
Index