[Agda] f (p1 , p2)

[Sergei Meshveliani]

Please,
how to make work the below pattern of    g {d} (p1 , p2) = ...
?
I have

----------------------------------------------------------------------
...
  private IncludedCommonDivs : C × C → C × C → Set (α ⊔ α=)
          IncludedCommonDivs (a , b) (a' , b') =
                             ∀ {d} → (d ∣ a × d ∣ b) → (d ∣ a' × d ∣ b')

  f : ∀ {x y} → IncludedCommonDivs (x , y) (x , y)
  f {d} (p1 , p2) = (p1 , p2)
  ...
  
  extGCD a b =  eGcd ...
    where
    a-eq :  a ≈ (a * 1#) + (b * 0#)
    ...

    eGcd u1 u2  ...  with v ≟ 0#
    ...
        | yes v=0 =  record{ ...}  where ...
    ... | no v≉0  =
          let
             (divRem′ q r u=q*v+r remLess) = divRem u v v≉0
             ...

             g : IncludedCommonDivs (a , b) (a , b)
             g {d} (p1 , p2) =  (p1 , p2)                              
             ...
          in
          ...
-----------------------------------------------------------------------

Now: 
1)  the pattern for  f  is type-checked,
2)  the pattern for  g  causes  "Not a valid let-declaration ..."

3)  the variant      g {d} pair =  (proj₁ pair , proj₂ pair)
    is type checked.                                      

I set `let' there because this allows the above pattern of   
            (divRem′ q r u=q*v+r remLess) = divRem u v v≉0.

Can this combination of  `with', `where' and `let' be reliable?  

I could try  `case' + `let',  with removing  `with' + `where'.
But 
a) `case' is often difficult to make it type-checked,
b) I doubt of whether the matter is in mixing  "with + let".

Thanks,

------
Sergei