{A B C P : Type} (f : TriJoinRecData A B C P) : TriJoinRecData' (j1 f) (j2 f) (j3 f) := Build_TriJoinRecData' (j1 f) (j2 f) (j3 f) (j12 f) (j13 f) (j23 f) (j123 f).
Require Import Basics Types.Paths WildCat Join.Core HoTT.Tactics.