module Two where

data  : Set where
  : 
  : 

not :   
not  = 
not  = 

open import Logic
open import Equality

two-equality-cases : {R : Ω}  
 ∀(b : )  (b    R)  (b    R)  R

two-equality-cases   f₀ f₁ = f₀ reflexivity
two-equality-cases   f₀ f₁ = f₁ reflexivity