proposition: Theorem cover_min_permutation : forall (t : btree A) (l1 l2 : list (btree A)), cover_min l1 t -> Permutation l1 l2 -> cover_min l2 t.
proof: Proof. intros t l1 l2 H H0; split. apply cover_permutation with (2 := H0); auto. inversion H; auto. intros t2 H1. assert (cover l1 t2). inversion H; auto. apply cover_permutation with (2 := Permutation_sym H0); auto. inversion H; auto. Qed.
imports: Coq(Sorting.Permutation)