fact: Definition lambda_calculus_rect_abs {L : lambda_calculus} {A f_var f_app f_abs f_subst f_paths n} l : lambda_calculus_rect (L := L) A f_var f_app f_abs f_subst f_paths n (abs l) = f_abs _ (lambda_calculus_rect _ f_var f_app f_abs f_subst f_paths _ l) := lambda_calculus_ind_abs l.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Tuples