proposition: Lemma IB_F2 rho : rho ⊫ F2.
proof: Proof. unfold F2. intros ? ([x y] & <- & ?) % in_map_iff u v ?. cbn. rewrite !IB_prep. cbn in *. eauto using der_sing, der_cons. Qed.
imports: Undecidability.PCP(PCP Util.PCP_facts) Undecidability.FOL(Deduction.FragmentNDFacts Semantics.Tarski.FragmentFacts Semantics.Tarski.FragmentSoundness Syntax.Core Syntax.Facts) Undecidability.FOL(FOL) Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ReducibilityFacts MoreReducibilityFacts) Undecidability.PCP.Reductions.PCPb_iff_dPCPb Undecidability(Shared.ListAutomation)