proposition: Lemma lambda_calculus_has_β : has_β lambda_calculus_lambda_theory.
proof: Proof. unfold has_β, LambdaTheories.app, LambdaTheories.abs. simpl. intros n l. rewrite inflate_abs. rewrite beta_equality. rewrite subst_subst. refine (_ @ subst_l_var _). apply maponpaths. apply funextfun. intro i. rewrite <- (homotweqinvweq stnweq i). induction (invmap stnweq i) as [i' | i']; refine (maponpaths (λ x, subst (_ x) _) (homotinvweqweq stnweq _) @ _); simpl. - do 2 rewrite inflate_var. rewrite subst_var. now rewrite extend_tuple_inl. - rewrite subst_var. now rewrite (extend_tuple_inr _ _ : extend_tuple _ _ lastelement = _). 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