proposition: Lemma saturated_P3 r x: equivalence r -> sub x (substrate r) -> (saturated r x <-> (x= inverse_direct_value (canon_proj r) x)).
proof: Proof. move=> er xs. set (p:=canon_proj r). have fp: function p by rewrite /p; fprops. split => h. apply: extensionality. by apply: inverse_direct_image =>//; rewrite /p; aw. move => y /(idvalue_cprojP er xs) [z [pa pb pc]]. move /(saturatedP er xs): h => q; move: (q _ pb); rewrite -pc. apply; fprops. apply/(saturatedP er xs); rewrite {2} h => y yx t tc. apply /(idvalue_cprojP er xs); split. exact: (sub_class_substrate er tc). ex_tac;exact:(class_eq2 er tc). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)