proposition: Lemma class_subst : forall (a : class) (G : cls) (x : term), typ_cls (cl_term x G) a -> forall (t : term) (k : nat) (E F : cls), TIns _ a k E F -> TTrunc _ k E G -> 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 Hlt ]. elim Hlt_eq; clear Hlt_eq. case n; simpl in |- *; [ intro Hlt | intro; intro 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. replace (cl_term (lift k x) E) with (cl_term x G). inversion_clear H; auto with coc core arith datatypes. symmetry in |- *. apply cl_trunc; auto with coc core arith datatypes. elim Tins_gt with class k E F Trm a n; auto with coc core arith datatypes. elim H0 with k E F; auto with coc core arith datatypes. elim H1 with (S k) (TCs class (cl_term t0 F) E) (TCs class (cl_term t0 F) F); auto with coc core arith datatypes. elim H0 with k E F; auto with coc core arith datatypes. elim H1 with k E F; auto with coc core arith datatypes. elim H0 with k E F; auto with coc core arith datatypes. elim H1 with (S k) (TCs class (cl_term t0 F) E) (TCs class (cl_term t0 F) F); auto with coc core arith datatypes. Qed.
imports: Termes Conv Types ListType