proposition: Lemma cl_term_subst : forall (a : class) (G : cls) (x : term), adj_cls (cl_term x G) a -> forall (t : term) (k : nat) (E F : cls), TIns _ a k E F -> TTrunc _ k E G -> loose_eqc (cl_term t F) (cl_term (subst_rec x t k) E).
proof: Proof. simple induction t; simpl in |- *; intros; auto with coc core arith datatypes. elim (lt_eq_lt_dec k n); simpl in |- *; [ intro Hlt_eq | intro lt ]. elim Hlt_eq; clear Hlt_eq. case n; simpl in |- *; [ intro Hlt | intros n0 Heq ]. inversion_clear Hlt. elim Tins_le with class k E F Trm a n0; auto with coc core arith datatypes. simple induction 1. rewrite (Tins_eq class k E F Trm a); auto with coc core arith datatypes. apply loose_eqc_trans with (cl_term x G). inversion_clear H; auto with coc core arith datatypes. elim cl_trunc with k E G x; auto with coc core arith datatypes. elim Tins_gt with class k E F Trm a n; auto with coc core arith datatypes. cut (loose_eqc (cl_term t0 F) (cl_term (subst_rec x t0 k) E)); intros; auto with coc core arith datatypes. cut (loose_eqc (cl_term t1 (TCs class (cl_term t0 F) F)) (cl_term (subst_rec x t1 (S k)) (TCs class (cl_term (subst_rec x t0 k) E) E))); intros. elim H5; auto with coc core arith datatypes; intros. elim H4; auto with coc core arith datatypes. apply loose_eqc_trans with (cl_term t1 (TCs _ (cl_term (subst_rec x t0 k) E) F)); auto with coc core arith datatypes. elim H0 with k E F; auto with coc core arith datatypes; intros. elim s1; elim s2; elim H1 with k E F; auto with coc core arith datatypes. cut (loose_eqc (cl_term t0 F) (cl_term (subst_rec x t0 k) E)); intros; auto with coc core arith datatypes. cut (loose_eqc (cl_term t1 (TCs class (cl_term t0 F) F)) (cl_term (subst_rec x t1 (S k)) (TCs class (cl_term (subst_rec x t0 k) E) E))); intros. elim H5; auto with coc core arith datatypes; intros. elim H4; auto with coc core arith datatypes. apply loose_eqc_trans with (cl_term t1 (TCs _ (cl_term (subst_rec x t0 k) E) F)); auto with coc core arith datatypes. Qed.
imports: Termes Conv Types ListType