proposition: Lemma translate_form_correct (f:falsity_flag) rho (phi : (@form _ _ full_operators f)) : (rho ⊨ translate_form phi <-> rho f⊨ phi).
proof: Proof. Proof using Ddec. apply correct. Qed.
imports: Vector Undecidability.FOL(Syntax.Facts) Undecidability.FOL.Semantics.Tarski(FullFacts FragmentFacts) Undecidability.FOL.Semantics.FiniteTarski(Full Fragment) Undecidability.Shared(Dec) Undecidability.Shared.Libs.PSL(Numbers) Coq(Arith Lia List) Undecidability.Shared.Libs.DLW.Wf(wf_finite) Undecidability.Synthetic(Definitions)