proposition: Lemma ins_in_cls : forall (c : class) (y : Int_K) (k : nat) (ipe ipf : intP), class_of_ik y = c -> TIns Int_K y k ipe ipf -> TIns _ c k (cls_of_int ipe) (cls_of_int ipf).
proof: Proof. unfold cls_of_int in |- *. simple induction 1. simple induction 1; simpl in |- *; auto with coc core arith datatypes. Qed.
imports: Termes Conv Types Class Can