proposition: Lemma cover_inv_app_aux : forall t t1 t2 l, cover l t -> t = node t1 t2 -> l = node t1 t2 :: [] \/ (exists l1, (exists l2, (cover l1 t1 /\ cover l2 t2) /\ Permutation l (l1 ++ l2))).
proof: Proof. intros t t1 t2 l H; elim H. intros t0 Ht0; rewrite Ht0; auto with datatypes. intros l1 l2 t0 t3 t4 H0 H1 H2 H3; right. case H2; auto. intros H4. exists (t1 :: []); exists (t2 :: []); simpl in |- *; repeat (split; auto). injection H4; intros H5 H6 H7; rewrite <- H5; rewrite <- H6; rewrite <- H7; auto. clear H2 H3; intros (l3, (l4, ((Hl1, Hl2), Hl3))). case (in_app_or l3 l4 (node t0 t3)). apply Permutation_in with (1 := Hl3); auto with datatypes. intros H2; case in_split with (1 := H2). intros l5 (l6, Hl5). exists (t0 :: t3 :: l5 ++ l6); exists l4; repeat (split; auto). apply cover_node with (l2 := l5 ++ l6) (t1 := t0) (t2 := t3); auto. apply cover_permutation with (1 := Hl1). rewrite Hl5. apply Permutation_trans with (node t0 t3 :: l6 ++ l5); try apply (Permutation_app_swap l5 (node t0 t3 :: l6)); auto. apply Permutation_trans with (1 := H0). simpl in |- *; repeat apply perm_skip. apply Permutation_cons_inv with (a := node t0 t3). apply Permutation_trans with (1 := Hl3). rewrite Hl5; auto. change (Permutation ((l5 ++ node t0 t3 :: l6) ++ l4) ((node t0 t3 :: l5 ++ l6) ++ l4)) in |- *. apply Permutation_app; auto. apply Permutation_trans with ((node t0 t3 :: l6) ++ l5); auto. simpl in |- *; auto. intros H2; case in_split with (1 := H2). intros l5 (l6, Hl5). exists l3; exists (t0 :: t3 :: l5 ++ l6); repeat (split; auto). apply cover_node with (l2 := l5 ++ l6) (t1 := t0) (t2 := t3); auto. apply cover_permutation with (1 := Hl2). rewrite Hl5. apply Permutation_trans with (node t0 t3 :: l6 ++ l5); try apply (Permutation_app_swap l5 (node t0 t3 :: l6)); auto. apply Permutation_trans with (1 := H0). apply Permutation_trans with ((t0 :: t3 :: l5 ++ l6) ++ l3); auto. simpl in |- *; repeat apply perm_skip. apply Permutation_cons_inv with (a := node t0 t3). apply Permutation_trans with (1 := Hl3). rewrite Hl5. apply Permutation_trans with ((l5 ++ node t0 t3 :: l6) ++ l3); auto. change (Permutation ((l5 ++ node t0 t3 :: l6) ++ l3) ((node t0 t3 :: l5 ++ l6) ++ l3)) in |- *; auto. apply Permutation_app; auto. apply Permutation_trans with ((node t0 t3 :: l6) ++ l5); auto. simpl in |- *; auto. Qed.
imports: Coq(Sorting.Permutation ArithRing)