We should replace `decreasing_by sorry` with proper termination proofs.
We should replace
decreasing_by sorrywith proper termination proofs.