Absurd Pattern

[KonjacSource]

data N : U where 
| Z : ... 
| S : (_:N) -> ...

data False : U where

data Id {A : U} : (x y : A) -> U where 
| refl : (t : A) -> ... t t 

fun what (add : N -> N -> N) (_ : Id (add Z Z) Z) : False where
| _ k !@ k

[KonjacSource]

Adding a new state for unification in pattern matching part, when unifying VCon with a non VCon. In this situation, we are not sure if it possible to use absurd pattern.