fact: Definition forgAr : forgOps -> choiceType := fun op => match op with |existT A _ => A end.
imports: Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples) Mon(SPropBase) mathcomp(all_ssreflect) Crypt(FreeProbProg ChoiceAsOrd)