proposition: Lemma compose_I2_abs_0_λ (a : lambda 2) : subst compose_λ (weqvecfun _ [(I2_λ ; abs (abs a))]) = abs (abs a).
proof: Proof. refine (_ @ compose_I2_abs_λ _). apply (maponpaths (λ x, _ (_ [(x ; _)]))). unfold I2_λ. do 2 rewrite subst_abs. rewrite subst_app. do 2 rewrite subst_var. extend_tuple_2. extend_tuple_1. now rewrite inflate_var. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.Tuples UniMath.Combinatorics.Vectors UniMath.Combinatorics.StandardFiniteSets UniMath.AlgebraicTheories.LambdaCalculus