I am trying to implement a simple type theory (typed lambda calculus with sums) like the one described in
Extensional Normalisation and Type-Directed Partial Evaluation for Typed Lambda Calculus with Sums
I wish to derive the following rule:
$$\begin{array}{c} \Gamma,x:A\vdash m:C\\ \overline{\Gamma,x:A\vdash\left(\left(\lambda x:A\right).m\right)\left(x\right)\equiv m:C} \end{array}$$
But the only approach I have thought of, is use the functional computation rule:
$$\begin{array}{c} \Gamma,x:A\vdash m:C\hspace{1em}\Gamma\vdash a:A\\ \overline{\Gamma\vdash\left(\left(\lambda x:A\right).m\right)\left(a\right)\equiv m\left[a/x\right]:C} \end{array}$$
together with weakening, to do a proof as follows:
$$ \begin{array}{c} \Gamma,x:A\vdash m:C\hspace{1em}\hspace{1em}\hspace{1em}\hspace{1em}\\ \underline{\overline{\Gamma,x:A,x:A\vdash m:C}\hspace{1em}\overline{\Gamma,x:A\vdash x:A}}\\ \Gamma,x:A\vdash\left(\left(\lambda x:A\right).m\right)\left(x\right)\equiv m:C \end{array} $$
But this reasoning involves including the repetition $x:A, x:A$ in the context, which I thought was not allowed (but I could be wrong).
I was hoping somebody could tell me if this is the right approach to proof, or if I am missing something. Another work around would be if the notation $\Gamma, x:A$ were interpreted as $\Gamma$ in the case where the type declaration $x:A$ is already in $\Gamma$.
I know I am focusing on small details, but I want to implement this theory in a computer program, and so I need to set things up very precisely.