proposition: Lemma exec_Iif_false: forall e cond p1 p2 e', (E.eval cond e)=false -> (exec e p2 e') -> (exec e (Iif cond p1 p2) e').
proof: Proof. intros e cond p1 p2 e' H1 H2. apply exec_Iif. rewrite H1; auto. Qed.
imports: hoarelogicsemantics partialhoarelogic totalhoarelogic