chore(library/logic/wf): remove unnecessary `:max`
test(tests/lean/run): define subterm relation for trees by hand
feat(frontends/lean/structure_cmd): generate no_confusion for structures too
test(tests/lean/run): define subterm relation for vectors
test(tests/lean/run): simple diag for square matrices
feat(library/data/vector): use 'mechanical' definitions, and add 'last' function

The 'mechanical' definitions are "mimicking" what the definitional
package will do.