proposition: Theorem forLoops_Inv_while2 : forall i:inst, forLoops i -> forall (b:bExp) (i':inst), i = WhileDo b i' -> forLoops i'.
proof: Proof. intros i h; case h; try (intros; discriminate). intros e i0 variant H H0 b i' H1; injection H1. intros heq2 heq1; rewrite <- heq2; assumption. Defined.
imports: ZArith Zwf Inverse_Image Wellfounded Extraction