I am quite new with the lambda calculus. I am experimenting lambda-calculus proofs through the coq proof assistant, but the question I have is not related to coq (I guess). However, I'm going to use the coq notation (It must be galina) to write lambda functions, such as (fun x:Z => x+ 1) which map (x+1) to x. (I use this notation because I don't know what is the general one). "nat" is the type of natural integers.
Let's consider I have a theorem that involve a lambda function (For example (fun x:nat => x+n) and n is any natural, defined in an hypothesis of the lemma) Let's suppose the theorem work directly on the lambda function (I'm probably using inappropriate words o.o), like for example (It is wrong, but I just use this example for the example) : the sum of any two lambda functions (that both return a natural) equals 0.
My question is : is it possible (I mean, strictly formally) to use an external lemma that would for example say $\forall a, b \in \mathbb{N}, a + b = 2$ (I know this is completely wrong, but it is just for the example).
So is it possible to use this lemma in the first theorem I have stated, to rewrite $x + n$ into $2$, according to the lemma.
I am asking this question for two reasons : I have almost no experience with lambda-calculus, and I am not sure at all about the variable decalarations ...
(The subject's title might not be appropriate .. I apologize if it is the case)
Thanks in advance !