2
module TerminationRecordPatternLie where
6
record Unit : Set where
15
record List (A : Set) : Set where
20
tail : T isCons -> List A
26
lie : {b : Bool} -> T b
28
f : {A : Set} -> List A -> Empty
29
f (list b h t) = f (t lie)
31
g : {A : Set} -> List A -> Empty