proposition: Lemma eq_succ x y : Gamma ⊢ (x == y) -> Gamma ⊢ (σ x == σ y).
proof: Proof. Proof using G. apply IE. 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