proposition: Lemma eq_add {x1 y1 x2 y2} : Gamma ⊢ (x1 == x2) -> Gamma ⊢ (y1 == y2) -> Gamma ⊢ (x1 ⊕ y1 == x2 ⊕ y2).
proof: Proof. Proof using G. intros H; apply IE. revert H; apply IE. apply Weak with FAeq. pose (sigma := [y2 ; y1 ; x2 ; x1] ∗ var). change (FAeq ⊢ _) with (FAeq ⊢ ($0 == $1 → $2 == $3 → $0 ⊕ $2 == $1 ⊕ $3)[sigma]). eapply subst_forall_prv with 4. apply Ctx. all: firstorder. repeat solve_bounds. Qed.
imports: Undecidability.FOL.Arithmetics(FA Signature) Undecidability.FOL(PA) Lia List Vector