proposition: Lemma UMP s1 s2 C : s1 \in C -> ~~ gen_dec C -> s1 = fAX s2^- -> exists x:UMType, suppC (val x) (s2^- |` R C).
proof: Proof. move => inC inDD E. subst s1. suff S: ~~ gen_dec (s2^- |` R C). case: (genN_supp S) => D D1 D2. by exists (Sub D D2). apply: contraNN inDD => /gen_decP H. rewrite (fset1U inC). apply/gen_decP. by constructor. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.K(K_def demo gentzen)