attempt to prove TRANS_correct, but going backwards

trying to work out a good definition of sequent, and the interplay with
has_meaning led me to realise that the syntactic inference system
probably needs to be different: it needs to be restricted to terms with
semantics only, but this has to be done by syntactic checks only
(probably by keeping track of what terms the kernel has produced).

indeed, the theorem REFL_correct proved before is useless for soundness,
since it assumes the term has_meaning, which the syntactic kernel won't
(and can't directly) check for.