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