Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- open import Data.Product
- open import Data.Unit
- open import Data.Empty
- postulate
- S D : Set
- A1 = S → ⊥
- A2 = D → ⊥
- A3 = (S → ⊥) × (D → ⊥) → ⊥
- postulate
- a1 : A1
- a2 : A2
- a3 : A3
- bad : ⊥
- bad = a3 ( a1 , a2 )
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
