proposition: Lemma class_is_inv_direct_value r x: equivalence r -> inc x (substrate r) -> class r x = inverse_direct_value (canon_proj r) (singleton x).
proof: Proof. move=> er xs. move: (set1_sub xs) => xs1. set_extens t => ts. apply/(idvalue_cprojP er xs1); split. exact: (sub_class_substrate er ts). exists x; fprops; exact :(class_eq2 er ts). move/(idvalue_cprojP er xs1): ts => [v [pa /set1_P <- <-]]; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)