proposition: Lemma symmetry x y : Gamma ⊢ (x == y) -> Gamma ⊢ (y == x).
proof: Proof. Proof using G. apply IE. apply (Weak FAeq). pose (sigma := [x ; y] ∗ var ). change (FAeq ⊢ _) with (FAeq ⊢ ($1 == $0 → $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