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; [ omega | ]. simpl. eapply IHe. omega. Qed.
imports: List Dblib(DblibTactics DeBruijn)