proposition: Lemma Σbpcp_model_dec : fo_model_dec Σbpcp_model.
proof: Proof. intros []; simpl; intros v; vec split v with x; vec split v with y; vec nil v; clear v; simpl; revert x y; intros [ (x & Hx) | ] [ (y & Hy) | ]; simpl; try tauto. + apply bpcp_hand_dec. + destruct (list_eq_dec bool_dec x y); destruct (is_a_tail_dec bool_dec y x); tauto. + destruct (list_eq_dec bool_dec x y) as [ | C ]; [ left | right ]. * subst; repeat f_equal; apply lt_pirr. * contradict C; inversion C; auto. + right; discriminate. + right; discriminate. 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)