Optlang: Some tidying up of tactics preamble
Optlang: Redo col_funs_rel proof