From 37a49513f22a3f792a1ac3241962a7d17455f7e5 Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Sat, 16 May 2020 09:02:13 +0900
Subject: A few more revisions

---
 mathcomp/ssreflect/finset.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp/ssreflect/finset.v')

diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v
index 9953c0d..e608d2b 100644
--- a/mathcomp/ssreflect/finset.v
+++ b/mathcomp/ssreflect/finset.v
@@ -900,7 +900,7 @@ Lemma subDset A B C : (A :\: B \subset C) = (A \subset B :|: C).
 Proof.
 apply/subsetP/subsetP=> sABC x; rewrite !inE.
   by case Bx: (x \in B) => // Ax; rewrite sABC ?inE ?Bx.
-by case Bx: (x \in B) => //; move/sABC; rewrite inE Bx.
+by case Bx: (x \in B) => // /sABC; rewrite inE Bx.
 Qed.
 
 Lemma subsetDP A B C :
-- 
cgit v1.2.3