∀ {F : PFunctor.{uA, uB}} {motive : (a : ℕ) → (a_1 a_2 : F.M) → PFunctor.M.Agree' a a_1 a_2 → Prop}
  {motive_1 : {a : ℕ} → {a_1 a_2 : F.M} → (t : PFunctor.M.Agree' a a_1 a_2) → PFunctor.M.Agree'.below t → Prop} {a : ℕ}
  {a_1 a_2 : F.M} {t : PFunctor.M.Agree' a a_1 a_2} (t_1 : PFunctor.M.Agree'.below t),
  (∀ (x y : F.M), motive_1 ⋯ ⋯) →
    (∀ {n : ℕ} {a : F.A} (x y : F.B a → F.M) {x' y' : F.M} (a_3 : x' = PFunctor.M.mk ⟨a, x⟩)
        (a_4 : y' = PFunctor.M.mk ⟨a, y⟩) (a_5 : ∀ (i : F.B a), PFunctor.M.Agree' n (x i) (y i))
        (ih : ∀ (i : F.B a), PFunctor.M.Agree'.below ⋯) (a_ih : ∀ (i : F.B a), motive n (x i) (y i) ⋯), motive_1 ⋯ ⋯) →
      motive_1 t t_1