proposition: Theorem cover_permutation : forall t l1 l2, cover l1 t -> Permutation l1 l2 -> cover l2 t.
proof: Proof. intros t l1 l2 H; generalize l2; elim H; clear H t l1 l2; auto. intros t l2 H; rewrite (Permutation_length_1_inv H); auto. intros l1 l2 t1 t2 t3 H H0 H1 l0 H2. apply cover_node with (2 := H0). apply Permutation_trans with (2 := H). apply Permutation_sym; auto. Qed.
imports: Coq(Sorting.Permutation ArithRing)