proposition: Lemma def_intp_can : forall e, can_adapt (def_intp e).
proof: Proof. simple induction e; simpl in |- *; auto with coc core arith datatypes; intros. unfold def_cons, int_cons, ext_ik in |- *. elim (cl_term a (cls_of_int (def_intp l))); auto with coc core arith datatypes. Qed.
imports: Termes Conv Types Class Can Int_term Int_typ Int_stab