proposition: Theorem unique_prefix_permutation : forall c1 c2 : code, Permutation c1 c2 -> unique_prefix c1 -> unique_prefix c2.
proof: Proof. intros c1 c2 H (H1, H2). cut (Permutation c2 c1); [ intros HP; split | apply Permutation_sym; auto ]. intros a1 a2 lb1 lb2 H0 H3 H4. apply (H1 a1 a2 lb1 lb2); auto. apply Permutation_in with (2 := H0); auto. apply Permutation_in with (2 := H3); auto. apply unique_key_perm with (2 := H2); auto. Qed.
imports: Coq(Sorting.Permutation)