proposition: Lemma I1_runit_λ (a : lambda 1) : subst compose_λ (weqvecfun 2 [( a ; inflate I1_λ )]) = subst compose_λ (weqvecfun 2 [( inflate I1_λ ; a )]).
proof: Proof. unfold compose_λ, I1_λ. do 2 refine (subst_abs _ _ @ !_). apply maponpaths. do 4 rewrite subst_app. rewrite inflate_abs. do 7 rewrite subst_var. extend_tuple_3. extend_tuple_3. cbn -[stnweq]. rewrite inflate_abs. do 2 rewrite beta_equality. extend_tuple_1. rewrite subst_var. rewrite extend_tuple_inr. do 2 rewrite subst_var. now do 2 rewrite extend_tuple_inr. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.Tuples UniMath.Combinatorics.Vectors UniMath.Combinatorics.StandardFiniteSets UniMath.AlgebraicTheories.LambdaCalculus