A B C : Join A (Join B C) <~> Join (Join A B) C. Proof. refine (_ oE trijoin_id_sym _ _ _). refine (_ oE equiv_trijoin_twist _ _ _). apply equiv_join_sym. Defined.
Require Import Basics Types WildCat Join.Core Join.TriJoin Spaces.Nat.Core.