Closed this issue 6 years ago · 1 comments
write a judgement that removes identity casts and argue that a term with only identity casts evaluates the same way as the term to which it is related by that judgement
did this in https://github.com/hazelgrove/hazelnut-dynamics-agda/blob/master/cast-inert.agda