fact: Definition ex5_coherent2 x := [/\ ex5_prodG (domain x) x, sub (domain x) (psI S) & forall K, finite_ne_sub K (domain x) -> ex5_coherent1 K (restr x K) ].
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)