Abstract_Soundness.Infinite_Proof_Soundness