proposition: Theorem fo_bisimilar_dec_congr : fo_congruence_upto (fun x y => x ≐ y) * (forall x y, decidable (x ≐ y)).
proof: Proof. Proof using fin dec. lsplit 3. + split; red; [ intros ? | intros ? ? ? | intros ? ?]; rewrite <- !fom_eq_fol_characterization; eauto. + intros ? ? ? ? ?; apply fom_eq_fol_characterization, fom_eq_syms_full; auto. intro; apply fom_eq_fol_characterization; auto. + intros ? ? ? ? ?; apply fom_eq_rels_full; auto. intro; apply fom_eq_fol_characterization; auto. + intros x y. destruct (fom_eq_dec x y); [ left | right ]; rewrite <- fom_eq_fol_characterization; auto. Qed.
imports: List Arith Nat Lia Relations Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat finite) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.FOL.TRAKHTENBROT(notations decidable gfp fol_ops fo_sig fo_terms fo_logic fo_definable fo_sat)