proposition: Lemma compose_I2_abs_λ {n : nat} (a : lambda (S (S n))) : subst compose_λ (weqvecfun _ [(subst I2_λ (weqvecfun _ vnil) ; abs (abs a))]) = abs (abs a).
proof: Proof. unfold compose_λ, I2_λ. do 3 rewrite subst_abs. do 3 rewrite subst_app. do 5 rewrite subst_var. extend_tuple_3. extend_tuple_2. extend_tuple_1. cbn -[stnweq]. rewrite inflate_var. do 2 rewrite inflate_abs. do 2 rewrite beta_equality. do 4 rewrite subst_abs. do 2 rewrite subst_subst. rewrite subst_app. do 2 rewrite subst_var. rewrite extend_tuple_inl. do 2 rewrite extend_tuple_inr. rewrite subst_var. rewrite inflate_var. rewrite extend_tuple_inr. rewrite subst_var. rewrite extend_tuple_inl. rewrite extend_tuple_inr. rewrite inflate_abs. rewrite beta_equality. do 2 rewrite subst_subst. do 2 apply maponpaths. 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 (subst (_ x) _) _) (homotinvweqweq stnweq _) @ _); cbn -[stnweq]. - rewrite subst_subst. unfold inflate. rewrite subst_subst. rewrite <- (homotweqinvweq stnweq i'). induction (invmap stnweq i') as [i'' | i'']; refine (maponpaths (λ x, subst (_ x) _) (homotinvweqweq stnweq _) @ _); cbn -[stnweq]. + do 4 rewrite subst_var. do 2 rewrite extend_tuple_inl. do 2 rewrite subst_var. rewrite extend_tuple_inl. do 3 rewrite subst_var. now rewrite extend_tuple_inl. + do 2 rewrite subst_var. rewrite extend_tuple_inl. rewrite extend_tuple_inr. do 2 rewrite subst_var. rewrite extend_tuple_inl. do 3 rewrite subst_var. now rewrite extend_tuple_inl. - rewrite subst_subst. rewrite subst_var. rewrite extend_tuple_inr. rewrite subst_var. rewrite extend_tuple_inr. 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