Post #2061449

@mei Being a decidable order is a proposition (if you don't know why, then... sub-puzzle!), so you can remove the truncation in "strong total order" when proving this.