ternary relations lemmas

[jonnybest]

as mentioned here

Ternary relations are constructed as (subset_3 R (prod_2x1 (prod_1x1 A B) C)). This may be a bad idea, especially since many joins are left joins: (join_1x3 (a2r_1 x) Rel3). It might be hard to reach the conclusion (in_1 x A) from this expression. I propose introducing a new lemma:

(= (subset_3 R (prod_2x1 (prod_1x1 A B) C)) (subset_3 R (prod_1x2 A (prod_1x1 B C)))