Derivation of term conversion rule

I've started to read Egbert Rijke's HoTT lecture notes which can be found here.

In the first lecture, some inference rules and structural rules are given, and in Exercise 1.1 it is asked to derive following term conversion rule using the rules given before:

If $$\Gamma \vdash A\equiv A'$$ type and $$\Gamma \vdash a:A$$, then $$\Gamma \vdash a:A'$$.

I'm not sure how can prove it formally. Here is my attempt:

Since $$A\equiv A'$$ in the context $$\Gamma$$, we have $$\Gamma \vdash A'$$. Using the variable rule, we gave $$\Gamma, x:A' \vdash x:A'$$ (1). Using the symmetry of judgmental equality of types, we have $$\Gamma \vdash A'\equiv A$$ (2). Using the conversion rule with generic judgment A/A' on (2) and (1), we obtain $$\Gamma, x:A \vdash x:A'$$ (3). Now, from (3) and $$\Gamma \vdash a:A$$, using substitution rule, we conclude $$\Gamma \vdash a:A'$$.

I'm not so familiar with the notation, so it can be written better. I hope, nevertheless, it makes sense to a reader. If someone gives a feedback or correction, it would be helpful.