proposition: Lemma Exercise1_3a13: E13_H2 -> bijection (fun_on_quotient E13_S E13_lam).
proof: Proof. move: Exercise1_3a9 => ffoq h2. have sfoq: source (fun_on_quotient E13_S E13_lam) = quotient E13_S. by rewrite /fun_on_quotient /section_canon_proj; aw. split; split => //. rewrite sfoq => x y xq yq. move: (Exercise1_3a12 h2 xq) (Exercise1_3a12 h2 yq). by move => [i [_ p1 p2]] [j [_ p3 p4]]; rewrite p2 p4 p1 p3; move => ->. rewrite sfoq {1} /fun_on_quotient; aw; rewrite -(Exercise1_3a3 h2) => y yd. set (a:= Vg (fam_of_substrates g) y *s1 y). have aq: (inc a (quotient E13_S)) by apply /(Exercise1_3a8P _ h2); ex_tac. ex_tac. move: (Exercise1_3a12 h2 aq) => [i [idg p1 ->]]. have h:= (setQ_repi Exercise1_3a7 aq); move: (h); rewrite {2} p1 => h1. by rewrite -(indexed_p2 h) -(indexed_p2 h1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)