proposition: Lemma Exercise3_2a E F: gfunctions E F = gfunctions F E -> E = F.
proof: Proof. move=> sEF. have pe: forall x E F, inc x F -> inc (cst_graph E x) (gfunctions E F). move => x a b xb; rewrite /gfunctions; aw. apply: Zo_i. by apply /setP_P; move => t /funI_P [z za ->]; apply:setXp_i. rewrite /cst_graph; split;aww. case: (emptyset_dichot E) => eE. case: (emptyset_dichot F) => eF; first by ue. move: eF => [x xE]; move: (pe x E F xE); rewrite sEF. by move => /Zo_P [_]; aw; move => [_ <-]. move: eE => [x xE]; move: (pe x F E xE); rewrite - sEF. by move => /Zo_P [_]; aw; move => []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)