Oh, so it’s equivalent to “S⊢¬□(DR(B =C))”. Everything makes sense now. At first I thought you were saying it was equivalent to the claim “to say B(DR =D), we would need S⊢¬□(DR(B =C))”, and I was confused.
Oh, so it’s equivalent to “S⊢¬□(DR(B =C))”. Everything makes sense now. At first I thought you were saying it was equivalent to the claim “to say B(DR =D), we would need S⊢¬□(DR(B =C))”, and I was confused.