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