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