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)))
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: