proposition: Lemma Add_rec x y : Gamma ⊢ ( (σ x) ⊕ y == σ (x ⊕ y) ).
proof: Proof. Proof using G. apply Weak with FAeq. pose (sigma := [y ; x] ∗ var). change (FAeq ⊢ _) with (FAeq ⊢ (σ $0 ⊕ $1 == σ ($0 ⊕ $1))[sigma]). eapply subst_forall_prv with 2. apply Ctx. all : firstorder. repeat solve_bounds. Qed.
imports: Undecidability.FOL.Arithmetics(FA Signature) Undecidability.FOL(PA) Lia List Vector