The key idea is to change the eutt_interp lemma. (The old one, which only allows rewriting the last argument is now called eutt_interp'), viewing interp as a higher-order morphism between handlers and itree morphisms. Then it should be possible to fold interp h t as apply_IFun (interp h) t, and then the proper lemma for apply_IFun (Indexed.FunctionFacts.Proper_apply_IFun) should allow you to rewrite h.
The idea suggested at the end of #101 goes a bit farther, to make apply_IFun the only way to apply interp h. Not sure whether that's worth the trouble.
Fix #101.
The key idea is to change the
eutt_interplemma. (The old one, which only allows rewriting the last argument is now calledeutt_interp'), viewinginterpas a higher-order morphism between handlers and itree morphisms. Then it should be possible to foldinterp h tasapply_IFun (interp h) t, and then the proper lemma forapply_IFun(Indexed.FunctionFacts.Proper_apply_IFun) should allow you to rewriteh.The idea suggested at the end of #101 goes a bit farther, to make
apply_IFunthe only way to applyinterp h. Not sure whether that's worth the trouble.