[Agda] rewrite vs. with

[David Leduc]

Hi,

Sorry, it's again a newbie question.
In the code below, I'd like to replace the hole in g with f b1 b2.
The problem is that f takes two arguments of the same type,
but the type of b1 and b2 are only provably equal (with Lemma eq).
In Coq I would use the tactic rewrite.
In Agda, I guess I should use a "with" but it does not work in this case.
I get the following error message:

  Cannot pattern match on constructor refl, since the inferred
  indices [proj1 t'] cannot be unified with the expected indices
  [proj2 t'] for some t', A'
  when checking that the expression ? has type A

What can I do?

--------------------------------

module test where

open import Relation.Binary.PropositionalEquality

data T (A : Set) : Set where
  makeT : (a1 a2 : A) -> a1 ≡ a2 -> T A

proj1 : {A : Set} -> T A -> A
proj1 (makeT a _ _) = a

proj2 : {A : Set} -> T A -> A
proj2 (makeT _ a _) = a

eq : {A : Set}(t : T A) -> proj1 t ≡ proj2 t
eq (makeT _ _ p) = p

g : (A : Set)(t : T A)(B : A -> Set)(f : B (proj1 t) -> B (proj1 t) -> A)
  (b1 : B (proj1 t))(b2 : B (proj2 t)) -> A
g A t B f b1 b2 with eq t
...| p = {!!}