proposition: Lemma nth_sub_inf : forall t T n e f, sub_in_env t T n e f -> forall v : nat, n > v -> forall u, item_lift u e v -> item_lift (subst_rec t u n) f v.
proof: Proof. simple induction 1. intros. inversion_clear H0. simple destruct v; intros. elim H3; intros. rewrite H4. inversion_clear H5. exists (subst_rec t u n0); auto with coc core arith datatypes. apply commut_lift_subst; auto with coc core arith datatypes. elim H3; intros. rewrite H4. inversion_clear H5. elim H1 with n1 (lift (S n1) x); intros; auto with coc core arith datatypes. exists x0; auto with coc core arith datatypes. rewrite simpl_lift; auto with coc core arith datatypes. pattern (lift (S (S n1)) x0) in |- *. rewrite simpl_lift; auto with coc core arith datatypes. elim H5. change (subst_rec t (lift 1 (lift (S n1) x)) (S n0) = lift 1 (subst_rec t (lift (S n1) x) n0)) in |- *. apply commut_lift_subst; auto with coc core arith datatypes. exists x; auto with coc core arith datatypes. Qed.
imports: Termes Conv MyList