| t : Bool ∈ (t : Bool , ∅) |
| t : Bool ∈ (n : (((Bool → Bool) → (Bool → Bool)) → ((Bool → Bool) → ((Bool → Bool) → Bool))) , (t : Bool , ∅)) |
| (n : (((Bool → Bool) → (Bool → Bool)) → ((Bool → Bool) → ((Bool → Bool) → Bool))) , (t : Bool , ∅)) ⊢ t : Bool |
| (t : Bool , ∅) ⊢ (λ n : (((Bool → Bool) → (Bool → Bool)) → ((Bool → Bool) → ((Bool → Bool) → Bool))) . t) : ((((Bool → Bool) → (Bool → Bool)) → ((Bool → Bool) → ((Bool → Bool) → Bool))) → Bool) |
| t : Bool ∈ (t : Bool , ∅) |
| t : Bool ∈ (t' : ((Bool → Bool) → (Bool → Bool)) , (t : Bool , ∅)) |
| t : Bool ∈ (y : (Bool → Bool) , (t' : ((Bool → Bool) → (Bool → Bool)) , (t : Bool , ∅))) |
| t : Bool ∈ (j : (Bool → Bool) , (y : (Bool → Bool) , (t' : ((Bool → Bool) → (Bool → Bool)) , (t : Bool , ∅)))) |
| (j : (Bool → Bool) , (y : (Bool → Bool) , (t' : ((Bool → Bool) → (Bool → Bool)) , (t : Bool , ∅)))) ⊢ t : Bool |
| (y : (Bool → Bool) , (t' : ((Bool → Bool) → (Bool → Bool)) , (t : Bool , ∅))) ⊢ (λ j : (Bool → Bool) . t) : ((Bool → Bool) → Bool) |
| (t' : ((Bool → Bool) → (Bool → Bool)) , (t : Bool , ∅)) ⊢ (λ y : (Bool → Bool) . (λ j : (Bool → Bool) . t)) : ((Bool → Bool) → ((Bool → Bool) → Bool)) |
| (t : Bool , ∅) ⊢ (λ t' : ((Bool → Bool) → (Bool → Bool)) . (λ y : (Bool → Bool) . (λ j : (Bool → Bool) . t))) : (((Bool → Bool) → (Bool → Bool)) → ((Bool → Bool) → ((Bool → Bool) → Bool))) |
| (t : Bool , ∅) ⊢ ((λ n : (((Bool → Bool) → (Bool → Bool)) → ((Bool → Bool) → ((Bool → Bool) → Bool))) . t) (λ t' : ((Bool → Bool) → (Bool → Bool)) . (λ y : (Bool → Bool) . (λ j : (Bool → Bool) . t)))) : Bool |
| ∅ ⊢ (λ t : Bool . ((λ n : (((Bool → Bool) → (Bool → Bool)) → ((Bool → Bool) → ((Bool → Bool) → Bool))) . t) (λ t' : ((Bool → Bool) → (Bool → Bool)) . (λ y : (Bool → Bool) . (λ j : (Bool → Bool) . t))))) : (Bool → Bool) |
| c : Bool ∈ (c : Bool , ∅) |
| (c : Bool , ∅) ⊢ c : Bool |
| ∅ ⊢ (λ c : Bool . c) : (Bool → Bool) |
|