proposition: Lemma WHILE_true_nonterm' : forall b c st st', bequiv b BTrue -> ~( (WHILE b DO c END) / st \\ st' ).
proof: Proof. MProof. intros b c. remember (WHILE b DO c END) "cw" "Heqcw". intros st st' eqT H. induction H &> except E_WhileEnd, E_WhileLoop do discriminate. - inversion Heqcw. subst. select (bequiv _ _) >>= unfold_in bequiv. move_back H. simpl. select (forall x:_, _) >>= rrewrite. simpl. discriminate. - select (WHILE _ DO _ END = _ -> _) >>= apply. assumption. Qed.
imports: Mtac2(Datatypes List Mtac2 ConstrSelector) Coq.Arith.Arith Coq.Arith.EqNat Strings.String