proposition: Lemma Exercise1_3a8P a: E13_H2 -> (inc a (quotient E13_S) <-> exists2 i, inc i (domain g) & a = (Vg (fam_of_substrates g) i) *s1 i).
proof: Proof. move: Exercise1_3a7 => es h2. have df : domain (fam_of_substrates g) = domain g. by rewrite /fam_of_substrates;aw. have aux: forall i, inc i (domain g) -> (Vg (fam_of_substrates g) i = substrate (Vg g i)). move=> i idg; rewrite /fam_of_substrates LgV//. split. move => aq; set y := rep a. have ysf: (inc y E13_sF) by rewrite -Exercise1_3a3'; apply: (rep_i_sr es aq). move: (disjointU_hi ysf); rewrite df; move => [Qx Px px];ex_tac. move/(setQ_P es): aq => aq. set_extens t. move => ta; move: (rel_in_class es aq ta) => /Exercise1_3a6P [_ tsf ->]. by move: (disjointU_hi tsf)=> [Qt Pt pt]; apply /indexed_P. move /indexed_P => [pt Pt Qt]; apply/(rel_in_class2 es aq). apply /Exercise1_3a6P;split => //; rewrite - pt Qt. by apply:disjoint_union_pi1 => //;rewrite - aux. move=> [i idg]; rewrite (aux _ idg) => ap; apply /(setQ_P es). have sa: sub a E13_sF. rewrite ap => t /indexed_P [pt Pt Qt]. by rewrite - pt Qt; apply: disjoint_union_pi1. have ra: inc (rep a) a. apply: rep_i; exists (J (rep (substrate (Vg g i))) i); rewrite ap. by apply: indexed_pi; apply: rep_i; apply: (proj2 h2). split; first by rewrite Exercise1_3a3'; apply: sa. have qa : Q (rep a) = i by rewrite {2} ap in ra; move: (indexed_p2 ra). set_extens t. move => ta; apply /(class_P es) /Exercise1_3a6P;split;fprops. by rewrite ap in ta; rewrite (indexed_p2 ta). move/(class_P es) /Exercise1_3a6P => [pa pb pc]; rewrite ap. move: (disjointU_hi pb) => [pd pe <-]; rewrite -pc qa. by apply : indexed_pi; rewrite - aux // -qa pc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)