proposition: Lemma lookup_beyond_length: forall A (e : env A) x, length e <= x -> lookup x e = None.
proof: Proof. induction e; simpl; intros. - eapply lookup_empty_None. - destruct x; [ lia | ]. simpl. eapply IHe. lia. Qed.
imports: List Arith Lia Dblib(DblibTactics DeBruijn)