From e669e531576b62447a8dc2f8342e2d82c2504ac8 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@csail.mit.edu>
Date: Mon, 15 Feb 2016 16:04:40 -0500
Subject: [PATCH] Reordering premises in Invariant theorems

---
 Invariant.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Invariant.v b/Invariant.v
index 36047f1..9c06c74 100644
--- a/Invariant.v
+++ b/Invariant.v
@@ -14,9 +14,9 @@ Definition invariantFor {state} (sys : trsys state) (invariant : state -> Prop)
                           -> invariant s'.
 
 Theorem use_invariant : forall {state} (sys : trsys state) (invariant : state -> Prop) s s',
-  sys.(Step)^* s s'
+  invariantFor sys invariant
+  -> sys.(Step)^* s s'
   -> sys.(Initial) s
-  -> invariantFor sys invariant
   -> invariant s'.
 Proof.
   firstorder.
@@ -24,8 +24,8 @@ Qed.
 
 Theorem invariantFor_monotone : forall {state} (sys : trsys state)
   (invariant1 invariant2 : state -> Prop),
-  (forall s, invariant1 s -> invariant2 s)
-  -> invariantFor sys invariant1
+  invariantFor sys invariant1
+  -> (forall s, invariant1 s -> invariant2 s)
   -> invariantFor sys invariant2.
 Proof.
   unfold invariantFor; intuition eauto.