improve the tactic $assumption
working on eta for nat