proposition: Theorem encode_app : forall l1 l2 c, encode c (l1 ++ l2) = encode c l1 ++ encode c l2.
proof: Proof. intros l1; elim l1; simpl in |- *; auto. intros a l H l2 c; rewrite H; auto. rewrite <- app_assoc; auto. Qed.
imports: Coq(Sorting.Permutation)