我是Agda的新手。我有以下代码要证明。现在我有问题lemma1c。 因为它要我证明z = a时z等于c。我有一个= c和c = c，以及trans函数。所以我想写

lemma1c = trans {z = a},{a = c}

但是我想让z不在范围内。我该怎么解决？

postulate
  A : Set
  a : A
  b : A
  c : A
  p : a ≡ b
  q : b ≡ c
  trans : ∀ {ℓ}{A : Set ℓ}{x y z : A} → x ≡ y → y ≡ z → x ≡ z
  trans refl refl = refl

  lemma0 : c ≡ c
  lemma0 = refl
  -- goal: c ≡ c,refl: x ≡ x
  lemma1a : a ≡ c
  lemma1a rewrite p = q

  lemma1c : ∀ {z : A} → z ≡ a → z ≡ c
  lemma1c {z} = trans {} {lemma1a}