proposition: Lemma tref_R0 C a : C \in U -> (forall D, D \in base S0 C -> gen (D,a)) -> gen (C,a).
proof: Proof. Proof using sfc_F. move: C. apply: @nat_size_ind _ _ (@weight _) _ => C IH inU. case: (posnP (weight C)) => [/weight0 lC |/weightS wC] B. - case (boolP (lcons C)) => L; last exact: lcons_gen. apply B. rewrite !inE suppxx; bcase. - have H (s : sform) (D : clause) : s \in C -> D `<=` (ssub s) -> (weight D < s_weight s) -> (forall E, suppC E D -> E |> s) -> gen (D `|` (C `\` [fset s]),a). move => inC sub_s wD sDs. apply IH. - by apply: fsum_replace; rewrite ?fsum1 ?fsub1. - rewrite powersetU [_ `\` _ \in _](@sub_power _ _ C) // andbT powersetE. apply: sub_trans sub_s _. apply: sf_ssub => //. rewrite powersetE in inU. exact: (subP inU). - move => E. rewrite !inE suppCU => /and3P [C1 C2 C3]. apply: B. rewrite !inE C1 /=. apply: suppCD C3. by rewrite suppC1 /= sDs. case/allPn : (wC). move => [[|p|s t|s|s] [|]] // inC _ ; rewrite -(fsetUD1 inC); constructor;rewrite ?fsetUA; (apply H => //; [Lsupp1|Lsupp2|Lsupp3]). Qed.
imports: Relations Lia mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype) CompDecModal.Kstar(Kstar_def demo hilbert_ref gen_def)