proposition: Theorem UM_universal s : (exists (M:cmodel) (w:M), eval s w) -> (exists (x:UM), eval s x).
proof: Proof. pose C := [fset s^+]. move => [M] [w Hw]. have: ~~ gen_dec C. apply: (@sat_cons M w) => ?. by rewrite in_fset1 => /eqP->. case/genN_supp => D /allP D1 D2. exists (Sub D D2). rewrite -[s]/(interp (s^+)). apply: supp_eval. apply: D1. exact: fset11. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.K(K_def demo gentzen)