proposition: Lemma Exercise3_2c E F: ordinalp (gfunctions E F) -> E = emptyset \/ F = emptyset.
proof: Proof. move=> bo; set T:= gfunctions E F. case: (emptyset_dichot F) => Fe; [ by right | left]. case: (equal_or_not emptyset T) => Te. move: Fe => [y yF];empty_tac1 (cst_graph E y). apply: Zo_i. by apply /setP_P => t /funI_P [z za ->]; apply:setXp_i. rewrite /cst_graph; split;aww. have: emptyset <o T by split => //; apply: (ole0x bo). by move /oltP0 => [_ _] /Zo_hi [_];rewrite domain_set0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)