proposition: Lemma option_rect_false_returns_true_iff {T} (f:T->bool) (o:option T) : option_rect (fun _ => bool) f false o = true <-> exists s:T, o = Some s /\ f s = true.
proof: Proof. unfold option_rect; split; [ destruct o; simpl; intro; try discriminate; eexists | intros [? [? ?]]; subst ]; eauto. Qed.
imports: Coq.Classes.Morphisms Coq.Relations.Relation_Definitions Fiat.Common.Coq__8_4__8_5__Compat