Automatic script generation fixed
Automatic script generation fixed

The new politics is to weaken binds in the thenll.
In particular, in (thenll t l), the new affine
binders generated by t (and only the new ones) at
the head of the new goals are removed.

Everything works, but it is hard to make composite
tactics. For example, forall_i can require or not
a bind depending if the variable occurs or not.
We need something more robust.

LPCIC/elpi