{A B C P} (f : TriJoinRecData A B C P) : TriJoinRecData A C B P. Proof. snrapply (Build_TriJoinRecData (j1 f) (j3 f) (j2 f)); intros. - apply (j13 f). - apply (j12 f). - symmetry; apply (j23 f). - cbn beta. apply moveR_pV; symmetry. apply (j123 f). Defined.
Require Import Basics Types WildCat Join.Core Join.TriJoin Spaces.Nat.Core.