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