fact: Definition restr_un_op (a : subcsetoid_crr) : subcsetoid_crr := match a with | Build_subcsetoid_crr x p => Build_subcsetoid_crr (f x) (pr x p) end.
imports: CoRN.tactics.CornTac CoRN.logic.CLogic CoRN.tactics.Step CoRN.algebra.RSetoid