proposition: Theorem forLoops_Inv_seq1 : forall i:inst, forLoops i -> forall i1 i2:inst, i = Scolon i1 i2 -> forLoops i1.
proof: Proof. intros i h; case h; try (intros; discriminate). intros i1 i2 H H0 i0 i3 H1; injection H1. intros heq2 heq1; rewrite <- heq1; assumption. Defined.
imports: ZArith Zwf Inverse_Image Wellfounded Extraction