proposition: Lemma compatible_constant_on_classes2 f r x: equivalence r -> compatible_with_equiv f r -> constantfp (restriction f (class r x)).
proof: Proof. move=> re [ff sf hyp]. have scs: sub (class r x) (substrate r) by apply: sub_class_substrate. rewrite - sf in scs. split; first by apply: (proj31 (restriction_prop ff scs)). have sr: source (restriction f (class r x)) = class r x. by rewrite /restriction; aw. rewrite sr. move=> a b ac bc /=; rewrite ! restriction_V //; apply: hyp. move: ac bc => /(class_P re) ac /(class_P re) bc; equiv_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)