fact: Definition switch_Eq c c' := match c' with | Eq => c | Lt => Lt | Gt => Gt end.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef