proposition: Theorem unique_prefix_not_null : forall (c : code) (a b : A), a <> b -> in_alphabet (a :: b :: []) c -> unique_prefix c -> not_null c.
proof: Proof. intros c a b H H0 H1. unfold not_null in |- *; intros a1; red in |- *; intros Ha1. case (H0 a); simpl in |- *; auto; intros l1 Hl1. case (H0 b); simpl in |- *; auto; intros l2 Hl2. case H; apply trans_equal with a1. apply sym_equal; apply unique_prefix1 with (3 := Hl1) (2 := Ha1); auto. apply unique_prefix1 with (3 := Hl2) (2 := Ha1); auto. Qed.
imports: Coq(Sorting.Permutation)