proposition: Theorem cover_app : forall t1 t2 l1 l2, cover l1 t1 -> cover l2 t2 -> cover (l1 ++ l2) (node t1 t2).
proof: Proof. intros t1 t2 l1 l2 H1; generalize t2 l2; elim H1; clear t1 t2 l1 l2 H1; simpl in |- *; auto. intros t t2 l2 H; apply cover_cons_l; auto. intros l1 l2 t1 t2 t3 H H0 H1 t0 l0 H2. apply cover_node with (l2 := l2 ++ l0) (t1 := t1) (t2 := t2); auto. apply Permutation_trans with ((t1 :: t2 :: l2) ++ l0); auto. Qed.
imports: Coq(Sorting.Permutation ArithRing)