Lambda the Ultimate

q-Derivatives of datatypes are partially applied functorial maps.

I am looking at the order theoretic axioms for intuitionistic propositional logic, which form a Heyting algebra. I am thinking about the join rule:

C ≤ A     C ≤ B
---------------
  C ≤ (A ^ B)

My understanding is the rule can be read both forwards and backwards. I initially encoded it like this:

rule(le(C, meet(A, B)), pair(le(C, A), le(C, B))).
rule(pair(le(C, A), le(C, B)), le(C, meet(A, B))).

But this needs the following additional rules to be defined:

rule(pair(A, B), pair(X, Y)) :- rule(A, X), rule(B, Y).
rule(pair(A, B), pair(Y, X)) :- rule(A, X), rule(B, Y).
rule(A, B) :- rule(A, C), rule(C,B).

The last of which is particularly problematic as it matches any 'A', and 'B' so results in dramatic increase in the search space, and results in a larger search depth to find the solution.

So as an alternative I want to encode the rules more natively, and I am thinking about extending the interpreter to allow conjunctions in the head, so the rules would be:

le(C, meet(A, B)) :- le(C, A), le(C, B).
le(C, A), le(C, B) :- le(C, meet(A, B)).

The implementation would match the first head struct as usual, and then would search the remaining goals for a match to the conjoined structs in the head (removing the matching goals).

Does this seem an efficient way to deal with this? Am I overlooking some way of rewriting the rules (although there is something to be said for keeping them close to the natural way of writing them)? Any suggestions for other ways to tackle this problem? I can't find any references to extending Prolog in this way, so I am concerned that this is problematic, or there is just a much simpler way to deal with it.