Step
*
of Lemma
fact0_redex_lemma
(0)! ~ 1
BY
{ (UnivCD THENA Auto) }
1
(0)! ~ 1
Latex:
Latex:
(0)! \msim{} 1
By
Latex:
(UnivCD THENA Auto)
Home
Index