proposition: Theorem cover_inv_app : forall t1 t2 l, cover l (node t1 t2) -> l = node t1 t2 :: [] \/ (exists l1, (exists l2, (cover l1 t1 /\ cover l2 t2) /\ Permutation l (l1 ++ l2))).
proof: Proof. intros t1 t2 l H; apply cover_inv_app_aux with (t := node t1 t2); auto. Qed.
imports: Coq(Sorting.Permutation ArithRing)