fact: Definition eq_semidec_and_gen {T} (semidec : forall x y : T, option (x = y)) (t t' : T) (f : T -> Type) (x : f t) (x' : f t') : option pointed_Prop := match semidec t t' with | Some p => Some (inject (eq_rect _ f x _ p = x')) | None => None end.
imports: Coq.Lists.List Coq.Arith.EqNat Coq.Logic.Eqdep_dec Fiat.Parsers.Reflective.Syntax Fiat.Parsers.Reflective.SyntaxEquality Fiat.Parsers.Reflective.SyntaxEquivalence Fiat.Common.PointedProp Fiat.Common.OptionFacts Fiat.Common.Prod Fiat.Common.Sigma Fiat.Common