proposition: Lemma inj_var_of_nat : forall m n : nat, var_of_nat m = var_of_nat n -> m = n.
proof: Proof. unfold var_of_nat in |- *. intros. apply dangerous_int_injection. apply ml_x_int_inj; auto with coc core arith datatypes. Qed.
imports: Arith MyList MlTypes