{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 _ _ _ _ _.
Require Import Basics Types.Paths WildCat Join.Core HoTT.Tactics.