proposition: Lemma prop_of_option_impl P Q : prop_of_option (impl_option_pointed_Prop P Q)%option_pointed_prop <-> (prop_of_option P -> prop_of_option Q).
proof: Proof. destruct P as [ [|P] |], Q as [ [|Q] |]; simpl; tauto. Qed.
imports: Coq.Setoids.Setoid Fiat.Common.Coq__8_4__8_5__Compat