Step
*
1
3
of Lemma
nat_add_mon_wf2
IsMonHomInj(<ℕ,+><ℤ+>λx.x)
BY
{ Auto }
Latex:
Latex:
IsMonHomInj(<\mBbbN{},+><\mBbbZ{}+>\mlambda{}x.x)
By
Latex:
Auto
Home
Index