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