proposition: Theorem encode_permutation : forall (m : list A) (c1 c2 : code), Permutation c1 c2 -> unique_prefix c1 -> encode c1 m = encode c2 m.
proof: Proof. intros m; elim m; simpl in |- *; auto. intros a l H c1 c2 H0 H1. apply f_equal2 with (f := app (A:=bool)); auto. apply find_code_permutation; auto. Qed.
imports: Coq(Sorting.Permutation)