add tactics

[c-cube]

• tactics are mostly in rust
• bridge to meta-language (where a tactic can be "applied" like a function or other builtins; composition operators)
• return a thm and a proof script, that is progressively built. This way you eventually get a proof script that can replace the tactic invocation.