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