fact: Definition and_pointed_Prop (x y : pointed_Prop) : pointed_Prop := match x, y with | trivial, y => y | x, trivial => x | inject p, inject q => inject (p /\ q) end.
imports: Coq.Setoids.Setoid Fiat.Common.Coq__8_4__8_5__Compat