fact: Definition trijoinrecdata_trijoin (A B C : Type) : TriJoinRecData A B C (Join A (Join B C)) := Build_TriJoinRecData join1 join2 join3 join12 join13 join23 join123.
imports: Basics Types.Paths WildCat Join.Core HoTT.Tactics