proposition: Lemma compatible_with_equiv_pr f r: function f -> source f = substrate r -> (compatible_with_equiv f r <-> (forall y, compatible_with_equiv_p (fun x => y = Vf f x) r)).
proof: Proof. move=> ff sf; rewrite/compatible_with_equiv/compatible_with_equiv_p. split. by move=> [_ _ hyp] y x x' => ->; apply: hyp. by move=> hyp; split => // x x'; apply: (hyp (Vf f x) x x'). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)