proposition: Lemma ins_item_ge : forall A n e f, ins_in_env A n e f -> forall v : nat, n <= v -> forall t, item _ t e v -> item _ t f (S v).
proof: Proof. simple induction 1; auto with coc core arith datatypes. simple destruct v; intros. inversion_clear H2. inversion_clear H3; auto with coc core arith datatypes. Qed.
imports: Termes Conv MyList