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