proposition: Lemma ins_item_lt : forall A n e f, ins_in_env A n e f -> forall v : nat, n > v -> forall t, item_lift t e v -> item_lift (lift_rec 1 t n) f v.
proof: Proof. simple induction 1. intros. inversion_clear H0. simple destruct v; intros. elim H3; intros. rewrite H4. exists (lift_rec 1 t n0); auto with coc core arith datatypes. inversion_clear H5. elim permute_lift with t n0; 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. pattern (lift (S (S n1)) x0) at 1 in |- *. rewrite simpl_lift; auto with coc core arith datatypes. elim H5. change (lift_rec 1 (lift (S (S n1)) x) (S n0) = lift 1 (lift_rec 1 (lift (S n1) x) n0)) in |- *. rewrite (permute_lift (lift (S n1) x) n0). unfold lift at 2 in |- *. pattern (lift (S (S n1)) x) in |- *. rewrite simpl_lift; auto with coc core arith datatypes. exists x; auto with coc core arith datatypes. Qed.
imports: Termes Conv MyList