proposition: Lemma compose_compose_2_λ {n : nat} (a b c d : stn n) : subst compose_λ (weqvecfun _ [( subst compose_2_λ (weqvecfun _ [(var a ; var b ; var c)]) ; var d )]) = subst compose_2_λ (weqvecfun _ [( var a ; subst compose_λ (weqvecfun _ [(var b ; var d)]) ; subst compose_λ (weqvecfun _ [(var c ; var d)]) )]).
proof: Proof. unfold compose_λ, compose_2_λ. rewrite (subst_abs (m := 3)). refine (compose_abs_λ _ _ _ @ _). do 8 rewrite subst_app. do 3 rewrite subst_abs. do 4 rewrite subst_subst. rewrite inflate_var. do 4 rewrite subst_var. do 8 rewrite subst_app. do 10 rewrite subst_var. do 2 extend_tuple_4. do 2 extend_tuple_3. cbn -[stnweq]. rewrite subst_var. do 4 rewrite inflate_var. do 2 rewrite inflate_abs. do 2 rewrite beta_equality. rewrite extend_tuple_inr. do 3 rewrite subst_var. do 8 rewrite subst_app. do 4 rewrite subst_subst. do 3 rewrite extend_tuple_inl. do 4 rewrite subst_var. do 3 rewrite extend_tuple_inl. rewrite extend_tuple_inr. rewrite subst_var. do 6 rewrite inflate_var. rewrite extend_tuple_inr. do 3 rewrite subst_var. now do 3 rewrite extend_tuple_inl. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.Tuples UniMath.Combinatorics.Vectors UniMath.Combinatorics.StandardFiniteSets UniMath.AlgebraicTheories.LambdaCalculus