proposition: Lemma has_beta_has_eta_preserves_abs {L L' : lambda_theory} {F : algebraic_theory_morphism L L'} (HL : has_β L) (HL' : has_η L') (Happ : ∏ n l, mor_app_ax F n l) (n : nat) (l : L (S n)) : mor_abs_ax F n l.
proof: Proof. refine (!HL' _ _ @ _). refine (maponpaths _ (!Happ _ _) @ _). 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