proposition: Lemma IB_F2 rho : rho ⊫ F2 R.
proof: Proof. unfold F2. intros ? ([x y] & <- & ?) % in_map_iff [u|] [v|] ?; cbn in *. - erewrite !IB_eval_Some; cbn; auto. now constructor 2. - erewrite IB_eval_Some, IB_eval_None; cbn; auto. - erewrite IB_eval_None; cbn; auto. - erewrite !IB_eval_None; cbn; auto. 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)