proposition: Lemma fgraph_setU2 a b: fgraph a -> fgraph b -> disjoint (domain a) (domain b) -> fgraph (a \cup b).
proof: Proof. move=> [fg fgg] [sg gfg] ei; split. move=> t; case/setU2_P; fprops. move=> x y; case/setU2_P => xab; case /setU2_P=> yab; first (by apply: fgg); last (by apply: gfg); move=> sp;empty_tac1 (P y); apply/funI_P; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)