Step
*
1
1
1
of Lemma
fact0_redex_lemma
1 ~ 1
BY
{ Try SqEqCD }
Latex:
Latex:
1  \msim{}  1
By
Latex:
Try  SqEqCD
Home
Index