proposition: Lemma lambda_calculus_is_algebraic_theory : is_algebraic_theory lambda_calculus_algebraic_theory_data.
proof: Proof. use make_is_algebraic_theory. - intros l m n f_l f_m f_n. revert l f_l m f_m n f_n. simpl. use (lambda_calculus_ind_prop (λ _ _, _ ,, _)); simpl. + do 4 (apply impred; intro). apply setproperty. + intros. now do 2 rewrite subst_var. + intros ? ? ? Hl Hl' ? ? ? ?. do 3 rewrite subst_app. now rewrite Hl, Hl'. + intros l f_l Hl m f_m n f_n. do 3 rewrite subst_abs. rewrite Hl. do 2 apply maponpaths. refine (!extend_tuple_eq _ _). * intro. refine (_ @ !maponpaths (λ x, subst x _) (extend_tuple_inl _ _ _)). rewrite inflate_subst. unfold inflate. rewrite subst_subst. apply maponpaths. apply funextfun. intro. rewrite subst_var. exact (!extend_tuple_inl _ _ _). * rewrite extend_tuple_inr, subst_var. exact (!extend_tuple_inr _ _). + intros m n l f Hl Hf m' f_m' n' f_n'. rewrite Hl. do 2 rewrite subst_subst. apply maponpaths. apply funextfun. intro. apply Hf. - do 4 intro. apply (subst_var i f). - use (lambda_calculus_ind_prop (λ _ _, _ ,, _)); simpl. + apply setproperty. + intros. apply subst_var. + intros ? ? ? Hl Hl'. now rewrite subst_app, Hl, Hl'. + intros n' l Hl. rewrite subst_abs. apply maponpaths. refine (_ @ Hl). apply maponpaths. exact (extend_tuple_eq inflate_var (idpath _)). + intros ? ? ? ? Hl Hf. rewrite subst_subst. apply maponpaths. apply funextfun. intro. apply Hf. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.StandardFiniteSets UniMath.AlgebraicTheories.AlgebraicTheories UniMath.AlgebraicTheories.AlgebraicTheoryCategoryCore UniMath.AlgebraicTheories.LambdaTheories UniMath.AlgebraicTheories.LambdaTheoryCategoryCore UniMath.AlgebraicTheories.LambdaCalculus UniMath.Combinatorics.Tuples