proposition: Lemma permut_nil : forall (A B : Type) (R : A -> B -> Prop) l, permut0 R l nil -> l = nil.
proof: Proof. intros A B R l P; inversion P as [ | a b l' l1 l2 a_R_b P']; trivial. destruct l1; discriminate. Qed.
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)