I'm new to Agda. I have the following code that I want to prove. Right now I have problem wit lemma1c.
since it wants me to prove when z = a, z will equal to c. and I have a = c and c = c, and the trans function. So I was trying to write 

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

```

but I want getting the z is not in scope error. How can I solve this?

```

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}

```