proposition: Lemma dangerous_int_injection : forall i j : nat, int_of_nat i = int_of_nat j -> i = j.
proof: Proof. simple induction i; simple destruct j; simpl in |- *; intros; auto. elim dangerous_discr with (int_of_nat n); auto. elim dangerous_discr with (int_of_nat n); auto. elim H with n0; auto. apply ml_int_pred; auto. Qed.