fact: Fixpoint isort A (r : relation A) l := match l with | nil => nil | x :: l => let l' := isort r l in filterP (fun y => r y x) l' ++ x :: filterP (fun y => ~ r y x) l' end.
imports: HahnBase HahnSets HahnList HahnRelationsBasic HahnEquational Sorted Setoid