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
It seems to me that adding the following rule to the system makes things simpler and more sensible:
$$\begin{array}{c} \underline{\Gamma\vdash a\equiv a':A}\\ \Gamma\vdash a:A \end{array}$$
But I am not sure if including this rule within the type theory is a good idea, and so I would like opinions about whether this rule can be added without causing logical issues.
The reason I want to add the above rule, is that some of the rules in the above reference introduce equal terms without declaring their types, and sometimes I seem to need to declare that such terms indeed have types, in order to do further operations upon them.