proposition: Theorem restrict_code_encode_length : forall (m : list A) (c : code A), encode A_eq_dec c m = encode A_eq_dec (restrict_code m c) m.
proof: Proof. intros m c; apply restrict_code_encode_length_inc; auto with datatypes. Qed.
imports: Coq(Sorting.Permutation)