fact: Definition trijoin_rec_beta_join12 {A B C P : Type} (f : TriJoinRecData A B C P) (a : A) (b : B) : ap (trijoin_rec f) (join12 a b) = j12 f a b := Join_rec_beta_jglue _ _ _ _ _.
imports: Basics Types.Paths WildCat Join.Core HoTT.Tactics