proposition: Lemma context_list_permut_cons : forall e l1 l2, list_permut l1 l2 -> list_permut (e :: l1) (e :: l2).
proof: Proof. intros e l1 l2; unfold list_permut, meq; simpl. intros H a; rewrite (H a); trivial. Qed.
imports: decidable_set List more_list Multiset Arith Setoid