proposition: Lemma permut_length : forall (A : Type) (R : relation A) l1 l2, permut0 R l1 l2 -> length l1 = length l2.
proof: Proof. intros A R l; induction l as [ | a l]; intros l' P; inversion P; trivial. subst. rewrite length_app; simpl; rewrite Nat.add_comm; simpl; rewrite Nat.add_comm. rewrite <- length_app; rewrite (IHl (l1 ++ l2)); trivial. Qed.
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)