FAQ
Known limitations

Mutual and even nested structural recursion are supported. Note that sometimes the automation can fail to prove the elimination principle due to the weakness of the syntactic guardedness criterion. In that case switching to a wellfounded induction can help. If it fails in case of nested recursion, one needs to craft the right elimination principle for the decreasing argument’s inductive type by hand.

The
dependent elimination
tactic is in active development, and does not have adependent induction
counterpart yet. 
We don’t try to automatically prove the completeness of the functions graph.