proposition: Lemma Exercise1_3a3: E13_H2 -> domain g = target E13_lam.
proof: Proof. move: Exercise1_3a1 => gE [gg alne]; rewrite /E13_lam /second_proj; aw. set_extens t. move=> tg;move: (alne _ tg) => [u us]; apply /(rangeP gE). by exists u; apply: disjoint_union_pi1. by move /(rangeP gE) => [x Je]; move: (du_index_pr1 Je); aw; case. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)