proposition: Lemma general_decider D (I:interp D) (e : env D) f : cListable D -> (forall (ff:falsity_flag) p v ee, dec (ee ⊨ atom p v)) -> dec (e ⊨ f).
proof: Proof. intros Hfin Hdec. induction f as [|f p v|f [] l IHl r IHr|f [] v IHv] in e|-*. - now right. - apply Hdec. - cbn. now apply and_dec. - cbn. now apply or_dec. - cbn. now apply impl_dec. - cbn. apply fin_dec. 1:easy. intros k. apply IHv. - cbn. apply fin_dec_ex. 1:easy. intros k. apply IHv. Qed.
imports: Undecidability.FOL.Semantics(Tarski.FullFacts) Undecidability.FOL.Syntax(Facts) Undecidability.Synthetic.DecidabilityFacts Undecidability.Shared.Dec List