{R : Type u} →
  {inst : Rack R} →
    {P : Sort u_1} →
      {x y x' y' : R} →
        ((Rack.PreEnvelGroup.incl x).mul (Rack.PreEnvelGroup.incl y)).mul (Rack.PreEnvelGroup.incl x).inv =
            ((Rack.PreEnvelGroup.incl x').mul (Rack.PreEnvelGroup.incl y')).mul (Rack.PreEnvelGroup.incl x').inv →
          Rack.PreEnvelGroup.incl (Shelf.act x y) = Rack.PreEnvelGroup.incl (Shelf.act x' y') →
            Rack.PreEnvelGroupRel'.act_incl x y ≍ Rack.PreEnvelGroupRel'.act_incl x' y' → (x ≍ x' → y ≍ y' → P) → P