proposition: Theorem unique_prefix_inv : forall (c : code) (a : A) (l : list bool), unique_prefix ((a, l) :: c) -> unique_prefix c.
proof: Proof. intros c a l (H1, H2); split. intros a1 a2 lb1 lb2 H H0 H3; apply (H1 a1 a2 lb1 lb2); simpl in |- *; auto. apply unique_key_inv with (1 := H2); auto. Qed.
imports: Coq(Sorting.Permutation)