• Recursion under binders
• Dependent case
• Expand until
• Clean duplicated hypothesis
• Assert if necessary
• RewriteAll
• RewriteAll, expert version
• Decide Equality