proposition: Lemma compose_I1_abs_0_λ (a : lambda 1) : subst compose_λ (weqvecfun _ [(I1_λ ; (abs a))]) = abs a.
proof: Proof. refine (_ @ compose_I1_abs_λ _). apply (maponpaths (λ x, _ (_ [(x ; _)]))). unfold I1_λ. rewrite subst_abs. rewrite subst_var. now extend_tuple_1. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.Tuples UniMath.Combinatorics.Vectors UniMath.Combinatorics.StandardFiniteSets UniMath.AlgebraicTheories.LambdaCalculus