proposition: Lemma int_typ_cr : forall (t : term) (ip : intP), can_adapt ip -> forall s : skel, is_can s (int_typ t ip _).
proof: Proof. simple induction t; simpl in |- *; intros; auto with coc core arith datatypes. generalize n. elim H; unfold Tnth_def in |- *; fold (Tnth_def Int_K) in |- *; intros. apply is_can_coerce; apply cand_sn. case n0; simpl in |- *; auto with coc core arith datatypes. inversion_clear H0; auto with coc; simpl in |- *; auto with coc. unfold def_cons, int_cons, ext_ik in |- *. elim (cl_term t0 (cls_of_int ip)); auto with coc core arith datatypes. case s; simpl in |- *; auto with coc core arith datatypes. elim (cl_term t1 (cls_of_int ip)); auto with coc core arith datatypes. intros. generalize (H ip H1 (PROD s0 s)); simpl in |- *; auto with coc core arith datatypes. case s; simpl in |- *; auto with coc core arith datatypes. apply is_can_Pi; simpl in |- *; intros; auto with coc core arith datatypes. unfold def_cons, int_cons, ext_ik in |- *. generalize X H2 H3. elim (cl_term t0 (cls_of_int ip)); auto with coc core arith datatypes. simpl in |- *. intros. change (is_can PROP (int_typ t1 (TCs Int_K (iK s0 X0) ip) PROP)) in |- *; auto with coc core arith datatypes. Qed.
imports: Termes Conv Types Class Can Int_typ