proposition: Lemma int_eq_can_cls : forall i i' : intP, int_eq_can i i' -> cls_of_int i = cls_of_int i'.
proof: Proof. unfold cls_of_int in |- *. simple induction 1; simpl in |- *; intros; auto with coc core arith datatypes. inversion_clear H0; simpl in |- *; intros; elim H2; auto with coc core arith datatypes. Qed.
imports: Termes Conv Types Class Can