proposition: Lemma equiv_perm : forall a n b p l l', equiv l l' -> equiv (cons a n (cons b p l))(cons b p (cons a n l')).
proof: Proof. intros a n b p l l' H c; simpl. case (T1_eq_dec c a); case (T1_eq_dec c b); simpl; case (H c); auto. intros;ring. Qed.
imports: Arith Omega ArithRing More_nat EPSILON0