totality014.idr:1:6-9:
  |
1 | data Con2 : Type where
  |      ~~~~
Universe inconsistency.
        Working on: ./totality014.idr.w
        Old domain: (5,5)
        New domain: (5,4)
        Involved constraints: 
                ConstraintFC {uconstraint = ./totality014.idr.w < ./totality014.idr.u, ufc = totality014.idr:1:6-9}
                ConstraintFC {uconstraint = ./totality014.idr.w < ./totality014.idr.u, ufc = totality014.idr:1:6-9}
                ConstraintFC {uconstraint = ./totality014.idr.u <= ./totality014.idr.w, ufc = totality014.idr:6:29}