Invalid actions (#101)

* Update coq-stdpp

* Update ChainStep to allow dropping invalid user actions

* Adapt proofs to new ChainStep

* More proofs updated

* Adapt ltacs in Blockchain.v to new ChainStep

* Update proofs in Circulation.v

* Update ltac in Blockchain.v

* no message

* Use intuition in proof

* Shorter proof without intuition

* Remove inhabited from step_action_invalid constructor

execution/theories/Blockchain.v

@@ -664,7 +664,7 @@ Inductive ChainStep (prev_bstate : ChainState) (next_bstate : ChainState) :=
       chain_state_queue prev_bstate = act :: acts ->
       chain_state_queue next_bstate = acts ->
       act_is_from_account act ->
-      (forall bstate new_acts, ~ inhabited (ActionEvaluation prev_bstate act bstate new_acts)) ->
+      (forall bstate new_acts, ActionEvaluation prev_bstate act bstate new_acts -> False) ->
       ChainStep prev_bstate next_bstate
 | step_permute :
       chain_state_env prev_bstate = chain_state_env next_bstate ->