{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) →
          t.ctorIdx = 2 →
            ({a b c : Rack.PreEnvelGroup R} →
                (hab : Rack.PreEnvelGroupRel' R a b) →
                  (hbc : Rack.PreEnvelGroupRel' R b c) → motive a c (hab.trans hbc)) →
              motive a a_1 t