proposition: Theorem weight_permutation : forall m c1 c2, unique_prefix c1 -> Permutation c1 c2 -> weight m c1 = weight m c2.
proof: Proof. intros m c1 c2 H H0; unfold weight in |- *. apply f_equal with (f := length (A:=bool)). apply encode_permutation; auto. Qed.
imports: Coq(Sorting.Permutation)