proposition: Lemma red_int_typ : forall (e : env) (U K : term), typ e U K -> forall ip : intP, cls_of_int ip = class_env e -> int_inv ip -> cl_term U (class_env e) <> Trm -> forall V : term, red U V -> eq_can (skel_int U ip) (int_typ U ip _) (int_typ V ip _).
proof: Proof. simple induction 5; auto with coc core arith datatypes; intros. apply eq_can_trans with (int_typ P ip (skel_int U ip)); auto with coc core arith datatypes. replace (skel_int U ip) with (skel_int P ip). apply int_typ_red1 with e K; auto with coc core arith datatypes. apply subject_reduction with U; auto with coc core arith datatypes. rewrite H0. elim class_red with e U P K; auto with coc core arith datatypes. unfold skel_int in |- *. rewrite H0. elim skel_sound with e U K; auto with coc core arith datatypes. elim skel_sound with e P K; auto with coc core arith datatypes. apply subject_reduction with U; auto with coc core arith datatypes. Qed.
imports: Termes Conv Types Class Can Int_typ