and sort them out in typing. Actually, there is no reason not
to have local lemmas.

Also, accept "let ghost (x,y) = ... in ...", which is the
same as "let x,y = ghost ... in ...", which is the same as
"match ghost ... with x,y -> ... end".