proposition: Lemma genN_supp C : ~~ gen_dec C -> exists2 D:clause, suppC D C & ~~ gen_dec D.
proof: Proof. move => H. suff: [some D in (S0 (sfc C)), suppC D C && ~~ gen_dec D]. { case/hasP => D _ /andP [D1 D2]. by exists D. } apply/negPn. rewrite -all_predC. apply: contraNN H => /allP H. apply/gen_decP. apply: (ref_R0 (@closed_sfc C)); first by rewrite powersetE sub_sfc. move => D /sepP [D1 D2]. move : (H _ D1) => /=. rewrite negb_and D2. by case: (gen_dec _). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.K(K_def demo gentzen)