∀ {R : Type u} [inst : Rack R] {motive : (a a_1 : Rack.PreEnvelGroup R) → Rack.PreEnvelGroupRel' R a a_1 → Sort u_1}
  {a a_1 : Rack.PreEnvelGroup R} (t : Rack.PreEnvelGroupRel' R a a_1)
  (F_1 :
    (a a_2 : Rack.PreEnvelGroup R) →
      (t : Rack.PreEnvelGroupRel' R a a_2) → Rack.PreEnvelGroupRel'.below t → motive a a_2 t),
  Rack.PreEnvelGroupRel'.brecOn t F_1 = F_1 a a_1 t (Rack.PreEnvelGroupRel'.brecOn.go t F_1).2