proposition: Lemma has_eta_has_beta_preserves_app {L L' : lambda_theory} {F : algebraic_theory_morphism L L'} (HL : has_η L) (HL' : has_β L') (Habs : ∏ n l, mor_abs_ax F n l) (n : nat) (l : L n) : mor_app_ax F n l.
proof: Proof. refine (!HL' _ _ @ _). refine (maponpaths _ (!Habs _ _) @ _). exact (maponpaths (λ x, _ (_ x)) (HL _ _)). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Tuples UniMath.AlgebraicTheories.AlgebraicTheories UniMath.AlgebraicTheories.AlgebraicTheoryMorphisms UniMath.AlgebraicTheories.AlgebraicTheoryCategoryCore UniMath.AlgebraicTheories.LambdaTheoryCategoryCore UniMath.AlgebraicTheories.LambdaTheories