proposition: Fact TM_sat_decidable {ff} (rho : nat -> unit) (phi : form ff) : rho ⊨ phi \/ ~(rho ⊨ phi).
proof: Proof. revert rho. induction phi as [|? ? ?|ff [| |] phi IHphi psi IHpsi|ff [|] phi IHphi]; cbn; intros rho; eauto; try tauto. - destruct (IHphi rho), (IHpsi rho); tauto. - destruct (IHphi rho), (IHpsi rho); tauto. - destruct (IHphi rho), (IHpsi rho); tauto. - destruct (IHphi (tt .: rho)). + left; now intros []. + right; intros Hcc. apply H, Hcc. - destruct (IHphi (tt .: rho)). + left; now exists tt. + right; now intros [[] Hx]. Qed.
imports: Undecidability.FOL.Syntax.Facts Undecidability.FOL.Semantics.Tarski.FullCore Undecidability(Shared.ListAutomation) Vector Lia