Lambda the Ultimate

I'm carrying out some experiments in theorem proving using combinator logic with equality, the rationale being that combinator logic is a variable-free substitute for lambda calculus, and getting rid of variables simplifies both semantics and code quite a bit.

I've run into a stumbling block for which suggests that I'm missing some inference rules, and would appreciate it if anyone could point me to what I'm missing. Here's what I have so far.

In first-order predicate calculus, practically all inference can be boiled down to two rules:

Unification: consistent substitution of terms for variables.
This would seem to be unnecessary in combinator logic, since there are no variables.

Paramodulation: free substitution of equals for equals.
This translates directly, and I have implemented it accordingly.

Lambda calculus adds a third rule:

Evaluation: expanding out a function call.
The obvious equivalent of this in combinator logic is expanding out full combinator calls, where I is given one argument, K is given two arguments or S is given three arguments; I have implemented this.

The simplest case on which the resulting system trips up is the set of clauses p(X) and ~p(X), which in first-order predicate calculus easily resolve to a contradiction. Translating these formulas and each step of the refutation proof into combinator logic gives (using Unlambda's ` notation, `a b means a(b)):

p(X)
p(X)=true
``eq ``s `k [p] i `k true

~p(X)
(p(X)=false)=true
``eq ``s ``s ``s `k s ``s ``s `k s ``s `k k `k eq `k i ``s `k k `k false ``s `k [p] i `k true

p(X) in the first statement unifies with p(X) in the second statement
p(X)=true, so in the second statement, substitute true for p(X)
(false=true)=true
``eq ``s ``s ``s `k s ``s ``s `k s ``s `k k `k eq `k i ``s `k k `k false `k true `k true

So far so good?
Now,
(false=true) trivially simplifies to false
But my program can't see how to simplify eq `k i ``s `k k `k false `k true and neither can I.

Why does (false=true) trivially simplify to false?
Because the inputs are constants not functions, and with constants, literal inequality means logical inequality
But the same is not true for functions
In the case of eq `k i ``s `k k `k false `k true the inputs to the equals comparison are functions, so there is no general rule that will determine they are unequal.

So what am I missing?

Hello everybody,

I ask you to excuse my ignorance in the question, I am a hobbyist programmer and I don't have any degree in CS. Recently I've found that some operations on types in advanced type systems are quite similar to logical operators.
For example, algebraic types are similar to exclusive OR operation, and multiple inheritance looks a lot loke AND operation.

I am sure this has been discovered and studied before (I can even remember reading about something similar in Wikipedia), but I cannot find any papers on the subject, probably because keywords like "type system" and "logical operators" do not really yield relevant results.

So, if such similarity exists, does it have a name? And what paper could you recommend that are relevant to this?