proposition: Lemma map_map_vanish: forall A B (f : B -> A) (g : A -> B) (e : env A), (forall x, f (g x) = x) -> map f (map g e) = e.
proof: Proof. induction e; intros; try match goal with o: option _ |- _ => destruct o end; simpl; eauto with f_equal. Qed.
imports: List Dblib(DblibTactics DeBruijn)