proposition: Lemma def_intt_id : forall n e k, def_intt e k n = Ref (k + n).
proof: Proof. simple induction n; simple destruct e; simpl in |- *; auto with coc core arith datatypes; intros. replace (k + 0) with k; auto with coc core arith datatypes. rewrite H. replace (k + S n0) with (S (k + n0)); auto with coc core arith datatypes. Qed.
imports: Termes Conv Types Class Can Int_term Int_typ Int_stab