proposition: Lemma Exercise1_3a12 x: E13_H2 -> inc x (quotient E13_S) -> exists i, [/\ inc i (domain g), x = (Vg (fam_of_substrates g) i) *s1 i & Vf (fun_on_quotient E13_S E13_lam) x = i].
proof: Proof. move: Exercise1_3a0 Exercise1_3a7 => fl es h2 xq. move /(Exercise1_3a8P x h2): (xq) => [i idg xp]. have sl:=proj2 Exercise1_3a3''. ex_tac. rewrite foqc_V //. have -> : Vf E13_lam (rep x) = Q (rep x). by rewrite /E13_lam second_proj_V // -Exercise1_3a3'; apply: rep_i_sr. have:(inc (rep x) x) by apply: (rep_in_class es); apply /(setQ_P es). by rewrite {2} xp; move /indexed_P => [_ _]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)