Logic and universe polymorphism

[Bas Spitters]

Some parts of this message have been removed. Learn more about Nabble's security policy.

With the introduction of universe polymorphism there seems to be a duplication of code:
"and" is just a special case of "prod"
...

This is awkward. For instance, if I define:
--
Infix "and" := prod (at level 80, right associativity).
(* This should replace iff in the standard library *)
Definition iff := fun A B : Type => (A -> B) and (B -> A).
Notation "A <-> B" := (iff A B) :type_scope.
--

A tactic like "apply <-" will not work for the new <->

What would be the best way to solve this?

Bas