∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} (r : β → γ → Prop) (_f : α → β) (_g : α → γ) (_f' : α → β)
  (_g' : α → γ),
  (l.germSetoid β) _f _f' →
    (l.germSetoid γ) _g _g' → (∀ᶠ (x : α) in l, r (_f x) (_g x)) = ∀ᶠ (x : α) in l, r (_f' x) (_g' x)