∀ {F : PFunctor.{uA, uB}} {R : F.M → F.M → Prop},
  PFunctor.M.IsBisimulation R →
    ∀ {a : F.A} {f f' : F.B a → F.M}, R (PFunctor.M.mk ⟨a, f⟩) (PFunctor.M.mk ⟨a, f'⟩) → ∀ (i : F.B a), R (f i) (f' i)