proposition: Lemma int_var_sound_lift : forall (t : term) (ip : intP) (i : Int_K), int_var_sound t ip i -> typ_cls (cl_term t (cls_of_int ip)) (class_of_ik i).
proof: Proof. intros. elim H; simpl in |- *; intros; rewrite H0; auto with coc core arith datatypes. Qed.
imports: Termes Conv Types Class Can Int_typ