proposition: Lemma prop_of_option_or P Q : prop_of_option (P \/ Q)%option_pointed_prop <-> (prop_of_option P \/ prop_of_option Q).
proof: Proof. destruct P, Q; simpl; autorewrite with push_to_prop; tauto. Qed.
imports: Coq.Setoids.Setoid Fiat.Common.Coq__8_4__8_5__Compat