Pp of scripts improved, but showstopper found
Pp of scripts improved, but showstopper found

We now try to turn the scripts into canonical form,
i.e. with "then" and pulling up "bind".

However, it is not working that well because too
much information is lost when pushing/erasing
binders. E.g.

then forall_i (bind _ x \ thenl t [ t1 , t2 ])

where x does not occur in the sequent proved by t2

when done interactively generates

thenl forall_i [ thenl (bind _ x \ t) [ bind _ x \ t1 , t2 ] ]

and we no longer know if the binder x is due to
the forall_i or to t. Therefore we cannot go back
to the nice script.

Another problem is the huge amount of complex code
introduced by this commit to "undo" something that
we did with another smaller amount of complex code.

We should try to restart and find a better solution,
maybe splitting the problem of pushing binders from
the one of erasing dummy abstractions that should be
hidden inside tactics. Conj is the example: we do
not want it to leave a dummy bind. Currently the
dummy binder was removed by push_bind.

LPCIC/elpi