proposition: Theorem encode_permutation_val : forall m1 m2 c, Permutation m1 m2 -> Permutation (encode c m1) (encode c m2).
proof: Proof. intros m1 m2 c H; elim H; simpl in |- *; auto; clear H m1 m2. intros; repeat rewrite app_assoc; auto. intros l1 l2 l3 H H0 H1 H2; apply Permutation_trans with (1 := H0); auto. Qed.
imports: Coq(Sorting.Permutation)