- | Use_ring_Luke
- | Use_fourier_Luke
- | Use_reflexivity_Luke
- | Use_symmetry_Luke
- | Use_assumption_Luke
- | Use_contradiction_Luke
- | Use_exists_Luke
- | Use_split_Luke
- | Use_left_Luke
- | Use_right_Luke
- | Use_apply_Luke of string (* use apply tactic on embedded term *)