proposition: Theorem encode_cons_inv : forall a l1 l m1, ~ In a m1 -> encode ((a, l1) :: l) m1 = encode l m1.
proof: Proof. intros a l1 l m1; generalize a l1 l; elim m1; simpl in |- *; auto; clear a l1 l m1. intros a l H a0 l1 l0 H0; case (A_eq_dec a a0); simpl in |- *; auto. intros H1; case H0; auto. intros e; rewrite H; auto. Qed.
imports: Coq(Sorting.Permutation)