add Poly_J.v
start Pair polymorphic section