proposition: Lemma opair_inj2 T x y x' y' : FSTeq <<= T -> T ⊢ opair x y ≡ opair x' y' -> T ⊢ y ≡ y'.
proof: Proof. intros HT H. assert (H' : T ⊢ y ≡ x' ∨ y ≡ y'). - assert (H2 : T ⊢ {x; y} ∈ opair x' y'). { eapply FST_eq_elem; trivial. apply FST_refl'; trivial. apply H. apply FST_pair_el'; trivial. apply DI2. now apply FST_refl'. } apply FST_pair_el' in H2; trivial. apply (DE H2). + apply DI1. apply FST_sym'; auto. eapply sing_pair2; auto. apply FST_sym'; auto. + apply FST_pair_el'; auto. eapply FST_eq_elem; auto. * apply FST_refl'; auto. * apply FST_pair_el'; auto. apply DI2. apply FST_refl'. auto. - apply (DE H'); try apply prv_T1. assert (H1 : T ⊢ x ≡ x') by apply (opair_inj1 HT H). assert (H2 : T ⊢ {x'; y'} ∈ opair x y). { eapply FST_eq_elem; trivial. apply FST_refl'; trivial. apply FST_sym', H; trivial. apply FST_pair_el'; trivial. apply DI2. now apply FST_refl'. } apply FST_pair_el' in H2; trivial. eapply DE; try eapply (Weak H2); auto. + eapply FST_trans'; auto. eapply FST_trans'; auto. * apply FST_sym'. auto. apply (Weak H1). auto. * eapply sing_pair2; auto. apply FST_sym'; auto. + eapply FST_trans'; auto. eapply sing_pair2; auto. eapply FST_trans'; auto. 2: apply FST_sym'; auto. eapply FST_eq_pair; try apply FST_sym'; auto. apply (Weak H1). auto. + auto. Qed.
imports: Undecidability.FOL.Syntax.Facts Undecidability.FOL.Semantics.Tarski.FullFacts Undecidability.FOL.Deduction.FullNDFacts Undecidability.FOL.Sets.FST Undecidability.FOL.FST Undecidability.FOL.Reductions.PCPb_to_FST Undecidability.PCP(PCP Util.PCP_facts Reductions.PCPb_iff_dPCPb) Undecidability(Shared.ListAutomation)