fact: Definition stable_test (f : sort_fun_t) {A} {le : relation A}{P: TotalPreOrder le} {dec:RelDecision le} (l: list A) : list (A * nat) := let m := mark l 0 in sort f (P:= @Total_Inverse_fun (A * nat) A fst le P) m.
imports: hydras(DecPreOrder_Instances)