Lifting again

[ghost]

In the following code

theorem foo:
  assume '⊤'
  theorem '∀x. x = x'
    let 'x'
    reflexive 'x'

my expectation is that foo should be a theorem ⊤ → ∀x. x = x, but instead, it is ∀ x. ⊤ → (x = x). I don't understand this. I'd have thought that when the inner theorem is lifted out of foo's context, it wouldn't get destructured so that an implication can be inserted inside the quantifier's body. Is this right?

[phlegmaticprogrammer]

By default lifting is "smart" (be aware of the danger whenever that word is used in a computer science context :-)), i.e. it is put into prenex normal form in each step. In your case that leads to the result you get. You could use theorem foo: true to avoid the smart stuff, and just do the literal stuff.

If that causes a lot of problems, we should have a discussion about this, especially because introducing a notion of goal as requested in #58 would shake things up considerably anyway. For example, it might not be wise to specify the lifting at the theorem level, but it should be specifiable at each proof statement.