Combinator equivalent to eta conversion
From the Barendregt lambda calculus book, we can find theory $CL$ (combinatory logic) defined as follows

$$
    K P Q = P \qquad
    S P Q R = P R (Q R)
$$

where $K,S$ are constant symbols (for the well known combinators), while $P,Q,R$ range over all the possible $CL$ terms (built from $K,S$, variables and application). The relation $=$ is postulated to be a congruence.

The $CL$ theory can be extended with the following $A_\beta$ axioms:

$$
\begin{array}{ll}
A.1 &amp; K = S(S(KS)(S(KK)K))(K(SKK)) \\
A.2 &amp; S = S(S(KS)(S(K(S(KS)))(S(K(S(KK)))S)))(K(K(SKK))) \\
A.3 &amp; S(S(KS)(S(KK)(S(KS)K)))(KK)=S(KK) \\
A.4 &amp; S(KS)(S(KK)) = \\
    &amp; \qquad S(KK)(S(S(KS)(S(KK)(SKK)))(K(SKK))) \\
A.5 &amp; S(K(S(KS)))(S(KS)(S(KS))) = \\
    &amp; \qquad S(S(KS)(S(KK)(S(KS)(S(K(S(KS)))S))))(KS)
\end{array}
$$

(I have double checked these, but I can't swear I got them right.)

Corollary 7.3.15 states that $CL\ +\ A_\beta$ is equivalent to $\lambda$ (the theory of the $\lambda$ calculus with $\beta$ conversion, but no $\eta$ or extensionality).

Hence, in principle one can use "only" the above laws to prove $SKK=SKS$.

The convenience of the above laws is self-evident, I think.

A similar set of axioms is found in the same book for $\lambda\eta = \lambda + \bf ext$. These are $A.3,A.4,A.5$ (hence no $A.1,A.2$) and

$$
\begin{array}{ll}
A.6 &amp; S(S(KS)K)(K(SKK)) = SKK
\end{array}
$$