proposition: Lemma cl_term_lift : forall (x : class) (t : term) (k : nat) (f g : cls), TIns _ x k f g -> cl_term t f = cl_term (lift_rec 1 t k) g.
proof: Proof. simple induction t; intros. simpl in |- *; auto with coc core arith datatypes. simpl in |- *. elim (le_gt_dec k n); simpl in |- *; intros. elim Tins_le with class k f g Trm x n; auto with coc core arith datatypes. elim Tins_gt with class k f g Trm x n; auto with coc core arith datatypes. simpl in |- *. elim H with k f g; auto with coc core arith datatypes. elim H0 with (S k) (TCs class (cl_term t0 f) f) (TCs class (cl_term t0 f) g); auto with coc core arith datatypes. simpl in |- *; auto with coc core arith datatypes. elim H with k f g; auto with coc core arith datatypes. elim H0 with k f g; auto with coc core arith datatypes. simpl in |- *. elim H with k f g; auto with coc core arith datatypes. elim H0 with (S k) (TCs class (cl_term t0 f) f) (TCs class (cl_term t0 f) g); auto with coc core arith datatypes. Qed.
imports: Termes Conv Types ListType