proposition: Theorem app_embed_right_triple : forall A B C (u : F A) (v : F B) (w : F C), u ** (v ** w) = right_triple <$> u <*> v <*> w.
proof: Proof. intros. unfold app_prod. repeat (rewrite <- app_fmap_unit). rewrite <- app_composition. f_equal. repeat (rewrite app_fmap_unit). rewrite fun_composition_x. repeat (rewrite <- app_fmap_unit). rewrite <- app_composition. f_equal. repeat (rewrite app_fmap_unit). rewrite fun_composition_x. rewrite app_interchange. rewrite app_fmap_unit. rewrite fun_composition_x. unfold compose. reflexivity. Qed.
imports: Endo Tuple Coq.Lists.List