Last active
August 11, 2016 17:06
Small change to exteq.v
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
diff --git a/exteq.v b/exteq.v | |
index a8fdd78..4a771bc 100644 | |
--- a/exteq.v | |
+++ b/exteq.v | |
@@ -31,13 +31,13 @@ cofix cf. destruct 1. constructor. apply cf. assumption. | |
Qed. | |
Lemma exteq_trans : | |
- forall s1 s2 s3, exteq s1 s2 -> exteq s2 s3 -> exteq s1 s3. | |
+ forall s1 s2 s3, exteq s2 s3 -> exteq s1 s2 -> exteq s1 s3. | |
Proof. | |
cofix cf. | |
intros (x1, s1) (x2, s2) (x3, s3) e12 e23. | |
case (exteq_inversion _ _ _ _ e12); clear e12; intros e12 ex12. | |
case (exteq_inversion _ _ _ _ e23); clear e23; intros e23 ex23. | |
-rewrite e12; rewrite e23. constructor. apply cf with s2; assumption. | |
+rewrite e23; rewrite e12. constructor. apply cf with s2; assumption. | |
Qed. | |
End sec_exteq. | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment