{α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      {δ : Type u_4} →
        {l : Filter α} →
          {lc : Filter γ} →
            (F : (α → β) → γ → δ) → Relator.LiftFun l.EventuallyEq lc.EventuallyEq F F → l.Germ β → lc.Germ δ