Abstract_Soundness.Finite_Proof_Soundness