∀ {R : Type u_1} [inst : Add R] [inst_1 : Mul R] {r : R → R → Prop}
  {motive : (a a_1 : R) → RingConGen.Rel r a a_1 → Prop}
  {motive_1 : {a a_1 : R} → (t : RingConGen.Rel r a a_1) → RingConGen.Rel.below t → Prop} {a a_1 : R}
  {t : RingConGen.Rel r a a_1} (t_1 : RingConGen.Rel.below t),
  (∀ (x y : R) (a : r x y), motive_1 ⋯ ⋯) →
    (∀ (x : R), motive_1 ⋯ ⋯) →
      (∀ {x y : R} (a : RingConGen.Rel r x y) (ih : RingConGen.Rel.below a) (a_ih : motive x y a), motive_1 ⋯ ⋯) →
        (∀ {x y z : R} (a : RingConGen.Rel r x y) (a_2 : RingConGen.Rel r y z) (ih : RingConGen.Rel.below a)
            (a_ih : motive x y a) (ih_1 : RingConGen.Rel.below a_2) (a_ih_1 : motive y z a_2), motive_1 ⋯ ⋯) →
          (∀ {w x y z : R} (a : RingConGen.Rel r w x) (a_2 : RingConGen.Rel r y z) (ih : RingConGen.Rel.below a)
              (a_ih : motive w x a) (ih_1 : RingConGen.Rel.below a_2) (a_ih_1 : motive y z a_2), motive_1 ⋯ ⋯) →
            (∀ {w x y z : R} (a : RingConGen.Rel r w x) (a_2 : RingConGen.Rel r y z) (ih : RingConGen.Rel.below a)
                (a_ih : motive w x a) (ih_1 : RingConGen.Rel.below a_2) (a_ih_1 : motive y z a_2), motive_1 ⋯ ⋯) →
              motive_1 t t_1