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 []. - exists (eval rho t). cbn. specialize (IHprv Heqp D I rho HA). apply sat_comp in IHprv. eapply sat_ext; try apply IHprv. now intros []. - edestruct IHprv1 as [d HD]; eauto. assert (H' : forall psi, phi = psi \/ psi el List.map (subst_form ↑) A -> (d.:rho) ⊨ psi). + intros P [<-|[psi'[<- H' % HA]] % in_map_iff]; trivial. apply sat_comp. apply H'. + specialize (IHprv2 Heqp D I (d.:rho) H'). apply sat_comp in IHprv2. apply IHprv2. - apply (IHprv Heqp) in HA. firstorder. - firstorder. - firstorder. - firstorder. now apply H0. - firstorder. now apply H0. - firstorder. - firstorder. - edestruct IHprv1; eauto. + apply IHprv2; trivial. intros xi [<-|HX]; auto. + apply IHprv3; trivial. intros xi [<-|HX]; auto. - discriminate. Qed.
imports: Undecidability.FOL.Syntax.Facts Undecidability.FOL.Semantics.Tarski.FullFacts Undecidability.FOL.Deduction.FullND Undecidability(Shared.ListAutomation) Vector Lia