[FOM] Simply Typed Lambda Calculus

[Steven Obua]

I have the following question concerning the simply typed 
(non-polymorphic) lambda calculus with constants and axioms for those 
constants.
The axioms are all of the form p = t, where p is a linear pattern and 
all the free variables in t are  bound by p. All the axioms are typed.

Assume that I have two terms A and B, both typed.

Assume further that I forget now about all types  and  use  beta , eta 
conversions  and the axioms  as if I would do in untyped lambda calculus.
Doing this, I manage to get from A to B.

My question is, can  I therefore also get from A to B if I DO NOT forget 
about the types but respect them? In particular, certain eta 
abstractions might not be possible that I could use
in the untyped setting but not in the typed setting.

I guess for type theorists this is a no-brainer. It would be great if 
someone could point me to an answer of this question in the literature.

Best,

Steven Obua