fact: Definition square_join_sym_assoc_twist A B C : functor_join (join_sym A B) idmap o join_assoc A B C == join_assoc B A C o trijoin_twist A B C.
imports: Basics Types WildCat Join.Core Join.TriJoin Spaces.Nat.Core