proposition: Lemma lookup_successor: forall A x (e : env A), lookup (S x) e = lookup x (tail e).
proof: Proof. destruct e. - do 2 rewrite lookup_empty_None. reflexivity. - reflexivity. Qed.
imports: List Arith Lia Dblib(DblibTactics DeBruijn)