fix: uncommitted proof

Author: jamesmckinna

src/Data/Fin/Properties.agda

@@ -568,7 +568,7 @@ lower₁≗lower {n = suc _ } zero    _   = refl
 lower₁≗lower {n = suc _ } (suc i) ne  = cong suc (lower₁≗lower i (ne ∘ cong suc))
 
 lower≗lower₁ : ∀ (i : Fin (suc n)) .(i<n : toℕ i ℕ.< n) →
-               lower i i<n ≡ lower₁ i {!ℕ.<⇒≢ i<n ∘ sym!}
+               lower i i<n ≡ lower₁ i (ℕ.<⇒≢ i<n ∘ sym)
 lower≗lower₁ {n = suc _ } zero    _   = refl
 lower≗lower₁ {n = suc _ } (suc i) lt  = cong suc (lower≗lower₁ i (ℕ.s<s⁻¹ lt))