proposition: Lemma def_adapt : forall e, wf e -> forall k, int_adapt e (def_intp e) (def_intt e k).
proof: Proof. simple induction e; simpl in |- *; intros. apply Build_int_adapt; auto with coc core arith datatypes. inversion_clear H0. cut (wf l); intros. elim H with (S k); trivial; intros in_interp ip_can_adapted same_classes. unfold def_cons, int_cons in |- *. apply Build_int_adapt; auto with coc core arith datatypes. apply int_cs; auto with coc core arith datatypes. apply (var_in_cand k (int_typ a (def_intp l) PROP)); auto with coc core arith datatypes. change (is_can PROP (int_typ a (def_intp l) PROP)) in |- *. apply int_typ_cr; auto with coc core arith datatypes. unfold ext_ik in |- *. rewrite same_classes. pattern (cl_term a (class_env l)) in |- *. apply class_typ_ord with s; auto with coc core arith datatypes. simpl in |- *. unfold ext_ik in |- *. rewrite same_classes. pattern (cl_term a (class_env l)) in |- *. apply class_typ_ord with s; unfold cls_of_int in |- *; elim same_classes; auto with coc core arith datatypes. simpl in |- *. rewrite same_classes. elim skel_sound with l a (Srt s); auto with coc core arith datatypes. simpl in |- *; auto with coc core arith datatypes. elim same_classes; auto with coc core arith datatypes. apply typ_wf with a (Srt s); auto with coc core arith datatypes. Qed.
imports: Termes Conv Types Class Can Int_term Int_typ Int_stab