proposition: Lemma all_big_substrate_prop g : all_big_substrate g -> exists f1 f2, [/\ inc f1 (prod_of_substrates g), inc f2 (prod_of_substrates g) & forall i, inc i (domain g) -> (Vg f1 i) <> (Vg f2 i)].
proof: Proof. move => ns. pose h v x := [/\ inc (P x) v, inc (Q x) v & P x <> Q x]. pose f0 i := choose (fun z => h (substrate (Vg g i)) z). have f0p: (forall i, inc i (domain g) -> h (substrate (Vg g i)) (f0 i)). move=> i idg; apply choose_pr. move: (ns _ idg); set t:= substrate (Vg g i) => ts. case:(emptyset_dichot t) => te; first by case:ts; move=> u v ue; empty_tac1 u. move: te=> [x xe]; case: (p_or_not_p (exists2 y, inc y t & x <> y)). by move=> [y yt yx]; exists (J x y); rewrite /h; aw. move => ep;case: ts; move=> u v /= ut vt; transitivity x. by symmetry; ex_middle xu; case: ep; exists u. by ex_middle xv;case: ep; exists v. exists (Lg (domain g) (fun i=> (P (f0 i)))). exists (Lg (domain g)(fun i => (Q (f0 i)))). split => //. by apply: prod_of_substrates_gi => i /f0p []. by apply: prod_of_substrates_gi => i /f0p []. by move => i idg; rewrite !LgV//; case: (f0p _ idg). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)