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