proposition: Lemma defined_implies_below_length: forall A (e : env A) x k a, length e <= k -> lookup x e = Some a -> x < k.
proof: Proof. intros. { case (le_gt_dec k x); intro; try tauto. - assert (lookup x e = None). eapply lookup_beyond_length. lia. congruence. } Qed.
imports: List Arith Lia Dblib(DblibTactics DeBruijn)