∀ {R : Type u_1} (motive : Rack.PreEnvelGroup R → Sort u_2) (h_1 : Unit → motive Rack.PreEnvelGroup.unit)
  (h_2 : (x : R) → motive (Rack.PreEnvelGroup.incl x)) (h_3 : (a b : Rack.PreEnvelGroup R) → motive (a.mul b))
  (h_4 : (a : Rack.PreEnvelGroup R) → motive a.inv),
  (match Rack.PreEnvelGroup.unit with
    | Rack.PreEnvelGroup.unit => h_1 ()
    | Rack.PreEnvelGroup.incl x => h_2 x
    | a.mul b => h_3 a b
    | a.inv => h_4 a) =
    h_1 ()