proposition: Lemma compose_2_term_1_λ : subst compose_2_λ (weqvecfun 3 [( subst term_1_λ (weqvecfun 1 [( var (make_stn 3 0 (idpath true)) )]); var (make_stn 3 1 (idpath true)); var (make_stn 3 2 (idpath true)) )]) = subst compose_λ (weqvecfun 2 [( var (make_stn 3 0 (idpath true)); subst term_2_λ (weqvecfun 2 [( var (make_stn 3 1 (idpath true)); var (make_stn 3 2 (idpath true)) )]) )]).
proof: Proof. unfold term_2_λ, compose_2_λ, compose_λ, term_1_λ. do 6 rewrite subst_abs. do 11 rewrite subst_app. rewrite subst_abs. do 12 rewrite subst_var. do 2 rewrite subst_app. do 3 rewrite subst_var. extend_tuple_4. extend_tuple_4. extend_tuple_3. extend_tuple_3. extend_tuple_2. extend_tuple_4_1. extend_tuple_4_2. extend_tuple_4_3. extend_tuple_3. cbn -[stnweq]. do 9 rewrite inflate_var. do 2 rewrite inflate_abs. do 2 rewrite beta_equality. do 4 rewrite subst_abs. do 2 rewrite subst_subst. rewrite beta_equality. do 6 rewrite subst_app. do 2 rewrite subst_abs. do 2 rewrite subst_subst. do 5 rewrite subst_var. do 2 rewrite subst_app. rewrite subst_subst. do 7 rewrite extend_tuple_inl. do 2 rewrite extend_tuple_inr. do 4 rewrite subst_var. do 10 rewrite inflate_var. do 3 rewrite extend_tuple_inl. do 4 rewrite extend_tuple_inr. do 6 rewrite subst_var. rewrite inflate_var. do 7 rewrite extend_tuple_inl. do 3 rewrite extend_tuple_inr. rewrite subst_var. do 5 rewrite inflate_var. rewrite extend_tuple_inl. rewrite extend_tuple_inr. do 2 rewrite subst_var. do 2 rewrite inflate_app. do 2 rewrite extend_tuple_inl. rewrite extend_tuple_inr. rewrite subst_app. do 4 rewrite inflate_var. rewrite inflate_app. do 2 rewrite subst_var. do 2 rewrite inflate_var. do 4 rewrite extend_tuple_inl. now do 2 rewrite inflate_var. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.Tuples UniMath.Combinatorics.Vectors UniMath.Combinatorics.StandardFiniteSets UniMath.AlgebraicTheories.LambdaCalculus