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