I would like some help choosing rules expressing that terms with an $\alpha$ conversion between them should be considered equal. I am trying to setup a typed lambda calculus with sums like in
Extensional Normalisation and Type-Directed Partial Evaluation for Typed Lambda Calculus with Sums
Except I am trying to explicitly express everything using inference rules.
$\alpha$ conversion is required for the two kinds of terms in the theory with bound expressions. For lambda abstractions I guess the $\alpha$ conversion rule should be
$$\begin{array}{c} \underline{\Gamma,x:A\vdash b:B\hspace{1em}\Gamma,y:A\vdash b':B\hspace{1em}\Gamma\vdash b\left[y/x\right]\equiv b':B}\\ \Gamma\vdash\left(\lambda x:A\right).b\equiv\left(\lambda y:A\right).b':A\rightarrow B \end{array}$$
where $y$ is free for $x$ in $b.$
For the terms $\text{match}\left(s,x.u,y.v\right)$ associated with sum types, as described in
I guess that the corresponding rules for $\alpha$ conversion should be
$\begin{array}{c} \underline{\Gamma\vdash s:A+B\hspace{1em}\Gamma,x:A\vdash u:C\hspace{1em}\Gamma,y:B\vdash v:C\hspace{1em}\Gamma,x':A\vdash u':C\hspace{1em}\Gamma\vdash u\left[x'/x\right]\equiv u':C}\\ \Gamma\vdash\text{match}\left(s,x.u,y.v\right)\equiv\text{match}\left(s,x'.u',y.v\right) : C \end{array}$
(where $x'$ is free for $x$ in $u$)
and
\begin{array}{c} \underline{\Gamma\vdash s:A+B\hspace{1em}\Gamma,x:A\vdash u:C\hspace{1em}\Gamma,y:B\vdash v:C\hspace{1em}\Gamma,y':B\vdash v':C\hspace{1em}\Gamma\vdash v\left[y'/y\right]\equiv v':C}\\ \Gamma\vdash\text{match}\left(s,x.u,y.v\right)\equiv\text{match}\left(s,x.u,y'.v'\right) : C \end{array}
(where $y'$ is free for $y$ in $v$).
Here, for a term $u,$ and a variable $x$ and a term $a,$ of the same type as $x,$ we write $u\left[a/x\right]$ to denote the result of taking term $u$ and replacing all free occurrences of $x$ with term $a.$ If no free variables of $a$ become bound in $u\left[a/x\right]$ then we say $a$ is free for $x$ in $u.$
My issue is that I am not sure if my guesses about how to formalize equality of $\alpha$ convertible terms are correct, and so I would appreciate it if somebody could tell me if I am correct, or say which rules I should use.