start proving invariant for initial state; currently it's not true

because the compiler puts Bind and Div in its initial environment as
constructors but they're not in the initial semantic constructor
environment. there may be other discrepancies too.