fact: Definition make_is_lambda_theory {L : lambda_theory_data} (app_comp : ∏ m n f g, app_comp_ax L m n f g) (abs_comp : ∏ m n f g, abs_comp_ax L m n f g) : is_lambda_theory L := app_comp ,, abs_comp.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Tuples UniMath.AlgebraicTheories.AlgebraicTheories UniMath.AlgebraicTheories.LambdaTheoryCategoryCore