Commit 2024-07-17 17:39 edf379e5
View on Github →feat: If s ≤ t in colex, then s \ {a} ≤ t \ {min t} in colex (#13827)
This proof is a horrible case bash. I have already spent a significant amount of time optimising it.
From LeanCamCombi
feat: If s ≤ t in colex, then s \ {a} ≤ t \ {min t} in colex (#13827)
This proof is a horrible case bash. I have already spent a significant amount of time optimising it.
From LeanCamCombi