1
module IrrelevantIndexNotInconsistent where
15
data D : .(b : Bool) → Set where
16
c : {b : Bool} → True b → D b
18
fromD : {b : Bool} → D b → True b
19
fromD (c p) = p -- should fail
21
cast : (a b : Bool) → D a → D b
25
bot = fromD (cast true false (c trivial))