lib_apply [1,1,1,1] refl [1, 1, 1, 1, 2]
⊢ MotivatedTree.Forall (Type u) fun X =>
    MotivatedTree.Forall (X → Set X) fun f =>
      MotivatedTree.Exists (Set X) fun a => MotivatedTree.Forall X fun a_1 => MotivatedTree.Not (a_1 ∈ f a_1) ↔ a_1 ∈ a
no goals