proposition: Lemma equiv_tail : forall a n l l', equiv (cons a n l) (cons a n l') -> equiv l l'.
proof: Proof. intros. unfold equiv;intros. generalize (H o). simpl. case (T1_eq_dec o a). intro;omega. auto. Qed.
imports: Arith Omega ArithRing More_nat EPSILON0