proposition: Theorem fmap_lookup_bk : forall a b m, mapsto a b (fmap_pmap m) -> exists b', mapsto a b' m /\ f b' = b.
proof: Proof. induction a; destruct m; simpl; intros; try congruence. { eapply IHa. eapply H. } { eapply IHa. eapply H. } { destruct o; try congruence. eexists; split; eauto. inversion H; auto. } Qed.
imports: ExtLib.Structures.Maps ExtLib.Structures.Functor ExtLib.Data.Option ExtLib.Data.Positive ExtLib.Tactics.Cases