As is, elimination with funelim is restricted to Prop. It seems to me that elimination into Type should be fine (since the underlying Acc allows elimination into Type).
Indeed. I actually generate eliminators into Type when the sort of the equality used is Type, but it shouldn’t depend on that. Maybe this kind of reports would be better placed on github issues 
That’s available in the 1.2beta2 version, and indeed can be useful to prove e.g. reflect predicates.
1 Like