Merge pull request #88 from volodeyka/master

Generalize `imfset_comp` lemma
math-comp · Jul 4, 2022 · 388f413 · 388f413
2 parents 6c6f3df + 6f0ae1a
commit 388f413
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/finmap.v b/finmap.v
@@ -2143,8 +2143,8 @@ Qed.
 End Enum.
 
 Section ImfsetTh.
-Variables (key : unit) (K V : choiceType).
-Implicit Types (f : K -> V) (g : V -> K) (A V : {fset K}).
+Variables (key : unit) (K V V' : choiceType).
+Implicit Types (f : K -> V) (g : V -> V') (A V : {fset K}).
 
 Lemma imfset_id (A : {fset K}) : id @` A = A.
 Proof. by apply/fsetP=> a; rewrite in_fset. Qed.