{α : Type u} →
  [inst : Mul α] →
    [inst_1 : One α] →
      {a : α} →
        {motive : Invertible a → Sort u_1} →
          (t : Invertible a) →
            ((invOf : α) →
                (invOf_mul_self : invOf * a = 1) →
                  (mul_invOf_self : a * invOf = 1) →
                    motive { invOf := invOf, invOf_mul_self := invOf_mul_self, mul_invOf_self := mul_invOf_self }) →
              motive t