proposition: Lemma compose_I1_abs_λ {n : nat} (a : lambda (S n)) : subst compose_λ (weqvecfun _ [(subst I1_λ (weqvecfun _ vnil) ; (abs a))]) = abs a.
proof: Proof. unfold compose_λ, I1_λ. do 2 rewrite subst_abs. rewrite subst_var. do 2 rewrite subst_app. do 3 rewrite subst_var. apply maponpaths. extend_tuple_3. cbn -[stnweq]. do 2 rewrite inflate_abs. do 2 rewrite beta_equality. extend_tuple_1. rewrite subst_var. rewrite extend_tuple_inr. rewrite subst_var. rewrite extend_tuple_inr. 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 _) @ _); cbn -[stnweq]. - do 2 rewrite inflate_var. rewrite subst_var. now rewrite extend_tuple_inl. - rewrite subst_var. now rewrite extend_tuple_inr. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.Tuples UniMath.Combinatorics.Vectors UniMath.Combinatorics.StandardFiniteSets UniMath.AlgebraicTheories.LambdaCalculus