namespace eta {

def0 Π : (A : ★) → (A → ★) → ★ = λ A B ⇒ (x : A) → B x

def0 function : (A : ★) → (B : A → Type) → (P : Π A B → ★) → (f : Π A B) →
                P (λ x ⇒ f x) → P f =
  λ A B P f p ⇒ p

def0 box : (A : ★) → (P : [ω.A] → ★) → (e : [ω.A]) →
           P [case1 e return A of {[x] ⇒ x}] → P e =
  λ A P e p ⇒ p

}