fact: Definition one_step (l1 l2 : list (btree A)) : Prop := exists l3 : list (btree A), (exists t1 : btree A, (exists t2 : btree A, ordered (sum_order f) (t1 :: t2 :: l3) /\ Permutation l1 (t1 :: t2 :: l3) /\ Permutation l2 (node t1 t2 :: l3))).
imports: Coq(Sorting.Permutation)