fact: Definition _mk_sum : forall {A B : Type'}, recspace (prod A B) -> sum A B := fun A B f => ε (fun p => f = _dest_sum p).
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat ProofIrrelevance