proposition: Lemma ex9_can_fun_ax i: inc i I -> lf_axiom (fun x => class ex9_rels_ext (J x i)) (Vg E i) ex9_quo.
proof: Proof. move: (chain_equivalence_eq) => [ha hb]. move => uI x xE; apply/ex9_quoP; apply: (class_class ha); rewrite hb. apply/ ex9G_P; split; aww. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)