書きかけだけれど、たぶん永遠に書きかけなので、とりあえず書いたところだけ公開。
idtac, fail, move, clear, set, remember, pose, rename, intro, assert, cut, lapply, specialize, generalizeexact, refine, applyconstructor, split, exists, left, rightabsurd, contradict, contradiction, exfalsofix, cofix, elim, induction, case (case_eq), destruct, intros, decompose, inversionreflexivity, symmetry, transitivity, decide equality, compare, discriminate, injection, congruence, f_equal, simplify_eqevar, instantiate, …cbv, lazy, compute, red, hnf, simpl, pattern, unfold, fold, rewrite, replace, subst, changeassumption, auto, trivial, tauto, intuition, rtauto, firstorder, omega, ring, ring_simplify, field, field_simplify, fourier, autorewrite