fact: Definition or_option_pointed_Prop (x y : option pointed_Prop) : option pointed_Prop := match x, y with | Some x, Some y => Some (or_pointed_Prop x y) | Some x, None => Some x | None, Some y => Some y | None, None => None end.
imports: Coq.Setoids.Setoid Fiat.Common.Coq__8_4__8_5__Compat