proposition: Lemma soundness {ff : falsity_flag} A phi : A ⊢I phi -> valid_ctx A phi.
proof: Proof. remember intu as p. induction 1; intros D I rho HA; comp. - intros Hphi. apply IHprv; trivial. intros ? []; subst. assumption. now apply HA. - now apply IHprv1, IHprv2. - intros d. apply IHprv; trivial. intros psi [psi'[<- H' % HA]] % in_map_iff. eapply sat_comp. now comp. - eapply sat_comp, sat_ext. 2: apply (IHprv Heqp D I rho HA (eval rho t)). now intros []. - apply (IHprv Heqp) in HA. firstorder. - firstorder. - discriminate. Qed.
imports: Undecidability.FOL.Syntax.Facts Undecidability.FOL.Semantics.Tarski.FragmentFacts Undecidability.FOL.Deduction.FragmentND Undecidability(Shared.ListAutomation) Vector Lia