proposition: Lemma int_equiv_int_typ : forall (T : term) (i i' : intP), int_eq_can i i' -> forall s : skel, eq_can s (int_typ T i s) (int_typ T i' s).
proof: Proof. simple induction T; simpl in |- *; intros; auto with coc core arith datatypes. generalize n. elim H; auto with coc core arith datatypes. unfold Tnth_def in |- *. intros. apply eq_can_extr. simpl in |- *; auto with coc core arith datatypes. simple destruct n0; intros; auto with coc core arith datatypes. unfold Tnth_def in |- *. inversion_clear H0; apply eq_can_extr || simpl in |- *; auto with coc core arith datatypes. simpl in |- *; auto with coc core arith datatypes. unfold def_cons, int_cons, ext_ik in |- *. elim int_eq_can_cls with i i'; auto with coc core arith datatypes. elim (cl_term t (cls_of_int i)); simpl in |- *; auto with coc core arith datatypes. case s; simpl in |- *; auto with coc core arith datatypes. unfold skel_int in |- *. elim int_eq_can_cls with i i'; auto with coc core arith datatypes. elim (cl_term t0 (cls_of_int i)); auto with coc core arith datatypes. intros. generalize (H i i' H1 (PROD s0 s)). unfold skel_int in |- *. simpl in |- *; intros. apply H2; auto with coc core arith datatypes. apply H0; auto with coc core arith datatypes. elim H1; intros; auto with coc core arith datatypes. inversion_clear H3; auto with coc core arith datatypes. apply H0; auto with coc core arith datatypes. elim H1; intros; auto with coc core arith datatypes. inversion_clear H3; auto with coc core arith datatypes. case s; simpl in |- *; auto with coc core arith datatypes. unfold int_cons, ext_ik in |- *. elim int_eq_can_cls with i i'; auto with coc core arith datatypes. apply eq_can_Pi; auto with coc core arith datatypes. simpl in |- *; intros. replace eq_cand with (eq_can PROP); auto with coc core arith datatypes. apply H0. pattern (cl_term t (cls_of_int i)) at 1 3 in |- *. elim (cl_term t (cls_of_int i)); auto with coc core arith datatypes. Qed.
imports: Termes Conv Types Class Can Int_typ