proposition: Lemma gen_lcons C : ~~ gen_dec C -> lcons C.
proof: Proof. apply: contraTT. rewrite negbK => ?. apply/gen_decP. exact: lcons_gen. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.K(K_def demo gentzen)