fact: Definition lambda_calculus_ind_app {L : lambda_calculus} {A f_var f_app f_abs f_subst f_paths n} (l l' : L n) : lambda_calculus_ind (L := L) A f_var f_app f_abs f_subst f_paths n (app l l') = f_app _ _ _ (lambda_calculus_ind _ f_var f_app f_abs f_subst f_paths _ l) (lambda_calculus_ind _ f_var f_app f_abs f_subst f_paths _ l') := pr122 L A f_var f_app f_abs f_subst f_paths n l l'.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Tuples