Type of suggested lemma in Bin-isomorphism compiles

Author: Jefferson Carpenter

src/plfa/part1/Quantifiers.lagda.md

@@ -493,7 +493,10 @@ Many of the alternatives for proving `to∘from` turn out to be tricky.
 However, the proof can be straightforward if you use the following lemma,
 which is a corollary of `≡Can`.
 
-    proj₁≡→Can≡ : {c c′ : ∃[ b ] Can b} → proj₁ c ≡ proj₁ c′ → c ≡ c′
+    proj₁≡→Can≡ : {c c′ : ∃[ b ] Can b} → Σ.proj₁ c ≡ Σ.proj₁ c′ → c ≡ c′
+
+We use the syntax `Σ.proj₁` to refer to the `proj₁` field defined in
+this module rather than to the imported `proj₁` field.
 
 ```agda
 -- Your code goes here