This is very good stuff.

This got me thinking that maybe Coq is not harder than Idris. Actually I think it is sometimes easier because Coq neatly separates proof from program when in Idris things get a bit mixed.