proposition: Lemma map_on_eq_some_inv : forall A B (f : A -> B) o x, map_on o f = Some x -> exists z, o = Some z /\ x = f z.
proof: Proof. Proof using. introv H. destruct o; simpl; inverts* H. Qed.
imports: TLC(LibTactics LibReflect)