fact: Definition stable (f : sort_fun_t) : Prop := forall (A B : Type) leA leB (PA : TotalPreOrder leA) (PB : TotalPreOrder leB) (dec : RelDecision leA) (l : list (A * B)), marked leA leB l -> marked leA leB (sort f (P:= Total_Inverse_fun (f:= fst : A * B -> A)) l).
imports: hydras(DecPreOrder_Instances)