proposition: Theorem Sig_bpcp_encode_complete : @fo_form_fin_dec_eq_SAT Σbpcp Σbpcp_eq eq_refl Σbpcp_encode -> exists l, lc ⊳ l∕l.
proof: Proof. intros (X & M & fM & dM & He & phi & Hphi). apply completeness with (M := M) (φ := phi); auto. Qed.
imports: List Arith Bool Lia Undecidability.PCP(PCP Util.PCP_facts) Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat finite) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.Shared.Libs.DLW.Wf(wf_finite) Undecidability.FOL.TRAKHTENBROT(notations utils bpcp fol_ops fo_sig fo_terms fo_logic fo_sat)