fact: Definition impl_option_pointed_Prop (x y : option pointed_Prop) : option pointed_Prop := match x, y with | None, _ => Some trivial | Some x, Some y => Some (impl_pointed_Prop x y) | Some p, None => not_option_pointed_Prop p end.
imports: Coq.Setoids.Setoid Fiat.Common.Coq__8_4__8_5__Compat