proposition: Lemma int_cons_equal : forall (ip : intP) (e : env), cls_of_int ip = class_env e -> forall (N : term) (s1 : sort), typ e N (Srt s1) -> forall C : Can (cv_skel (cl_term N (class_env e))), cls_of_int (int_cons N ip _ C) = class_env (N :: e).
proof: Proof. intros. unfold int_cons, ext_ik in |- *. rewrite H. simpl in |- *. generalize C. pattern (cl_term N (class_env e)) in |- *. apply class_typ_ord with s1; auto with coc core arith datatypes. simpl in |- *; intros. elim skel_sound with e N (Srt s1); simpl in |- *; intros; auto with coc core arith datatypes. unfold cls_of_int in |- *; simpl in |- *; elim H; auto with coc core arith datatypes. unfold cls_of_int in |- *; simpl in |- *; elim H; auto with coc core arith datatypes. Qed.
imports: Termes Conv Types Class Can Int_typ