proposition: Theorem NoDup_ordered_cover : forall l1 l2 t, ordered_cover l1 t -> NoDup l2 -> l1 = map (fun x : A => leaf x) l2 -> all_leaves t = l2.
proof: Proof. intros l1 l2 t H; generalize l2; elim H; clear H l1 l2 t; simpl in |- *; auto. intros t l l2; case l2; simpl in |- *; auto. intros; discriminate. intros a0 l0 H H0; injection H0; intros H1 H2; rewrite H2; auto. generalize H1; case l0; simpl in |- *; auto. intros; discriminate. intros t1 t2 l1 l2 l3 H H0 H1 H2 l0 H3 H4. cut ((exists l3 : list A, l1 = map (fun x : A => leaf x) l3) /\ (exists l4 : list A, l2 = map (fun x : A => leaf x) l4)). intros ((l4, HH1), (l5, HH2)). cut (l0 = l4 ++ l5); [ intros HH3 | idtac ]. rewrite HH3. apply f_equal2 with (f := app (A:=A)). apply H0; auto. apply NoDup_app_inv_l with (l2 := l5); rewrite <- HH3; auto. apply H2; auto. apply NoDup_app_inv_r with (l1 := l4); rewrite <- HH3; auto. rewrite HH2 in H4; rewrite HH1 in H4. rewrite <- map_app in H4. generalize H4; generalize (l4 ++ l5); elim l0; simpl in |- *; auto. intros l; case l; simpl in |- *; auto. intros; discriminate. intros a0 l H5 l6; case l6; simpl in |- *; auto. intros; discriminate. intros a1 l7 H6; apply f_equal2 with (f := cons (A:=A)); auto. injection H6; auto. injection H6; auto. generalize H4; generalize l2 l0; elim l1; simpl in |- *; auto. intros l4 l5 H5; split; [ exists [] | exists l5 ]; auto. intros a0 l H5 l4 l5; case l5; simpl in |- *; auto. intros; discriminate. intros a1 l6 H6; case (H5 l4 l6); auto. injection H6; auto. intros (l7, HH5) (l8, HH6); split; [ exists (a1 :: l7) | exists l8 ]; simpl in |- *; auto. apply f_equal2 with (f := cons (A:=btree A)); auto. injection H6; auto. Qed.
imports: Coq(Sorting.Permutation)