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