proposition: Theorem equivalence_perm : equivalence _ perm.
proof: Proof. split. - intro x;constructor 2. - intros x y z;constructor 3 with y;auto. - intros x y H; induction H. + constructor 1;apply transpose_sym;assumption. + constructor 2. + constructor 3 with y;auto. Qed.
imports: Relations List Operators_Properties