proposition: Theorem length_encode_nId : forall a l1 l n, length (encode A_eq_dec ((a, l1) :: l) (id_list a n)) = n * length l1.
proof: Proof. intros a l1 l n; elim n; simpl in |- *; auto. intros n0 H; case (A_eq_dec a a); auto. intros e; rewrite app_length; rewrite H; auto. intros H1; case H1; auto. Qed.
imports: Coq(Sorting.Permutation)