fact: Definition trijoin_id_sym_nat {A B C A' B' C'} (f : A -> A') (g : B -> B') (h : C -> C') : trijoin_id_sym A' B' C' o functor_join f (functor_join g h) == functor_join f (functor_join h g) o trijoin_id_sym A B C.
imports: Basics Types WildCat Join.Core Join.TriJoin Spaces.Nat.Core