title: Substituting equal term in equality proof
body: <p>I have the following definition</p>
  
  <pre><code>open import Relation.Binary.PropositionalEquality
  
  data _≅_ (A B : Set) : Set where
    mkBij : (f : A → B) (g : B → A)
            → (∀ a → a ≡ g (f a))
            → (∀ b → b ≡ f (g b))
            → A ≅ B
  </code></pre>
  
  <p>And I'm trying to show transitivity. I have what I need, but I don't know how to combine them to get the proof object I want. This is the proof so far.</p>
  
  <pre><code>transtv : ∀ {A B C} → A ≅ B → B ≅ C → A ≅ C
  transtv (mkBij f₁ g₁ x y) (mkBij f₂ g₂ w z) =
    mkBij (λ x₁ → f₂ (f₁ x₁)) (λ z₁ → g₁ (g₂ z₁))
          (λ a → let xa = x a
                     wb = w (f₁ a)
                 in {!!})
          (λ c → let zc = z c
                     yb = y (g₂ c)
                 in {!!})
  </code></pre>
  
  <p>In the first hole, I have these: (the second hole is identical)</p>
  
  <pre><code>Goal: a ≡ g₁ (g₂ (f₂ (f₁ a)))
  wb : f₁ a ≡ g₂ (f₂ (f₁ a))
  xa : a ≡ g₁ (f₁ a)
  </code></pre>
  
  <p>Now, it's obvious that if I replace <code>f₁ a</code> with <code>g₂ (f₂ (f₁ a))</code> in <code>xa</code> I get to the goal. But I don't know how to do this substitution in agda. What kind of function or language construct do I need to do this?</p>