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