exact, refine, intros, apply
hnf, cbn, cbv, unfold, fold, change, pattern
reflexivity, rewrite, f_equal, symmetry, transitivity, replace
constructor, destruct, induction, discriminate, injection
split, left, right, exfalso, contradict, exists
revert, clear, assert, enough, specialize, generalize, pose, set
assumption, trivial, easy, subst, auto
lia, nia, tauto, congruence, intuition, firstorder, decide equality
eapply, eexists, eassumption, eauto
”;”, now, repeat, try, unshelve