proposition: Theorem ixapp_embed_right_triple : ∀ I J K L A B C (u : F I J A) (v : F J K B) (w : F K L C), u ** (v ** w) = right_triple <$$> u <**> v <**> w.
proof: Proof. intros. unfold ixapp_prod. repeat (rewrite <- app_ixmap_unit). rewrite <- ixapp_composition. repeat (rewrite app_ixmap_unit). rewrite ixfun_composition_x. repeat (rewrite <- app_ixmap_unit). rewrite <- ixapp_composition. repeat (rewrite app_ixmap_unit). rewrite ixfun_composition_x. rewrite ixapp_interchange. rewrite app_ixmap_unit. rewrite ixfun_composition_x. unfold comp. reflexivity. Qed.
imports: Hask.Ltac Coq.Program.Equality Coq.Unicode.Utf8 FunctionalExtensionality Iso Tuple