proposition: Lemma compose_F_λ : subst compose_λ (weqvecfun 2 [( subst F_λ (weqvecfun 0 [()]); subst term_2_λ (weqvecfun 2 [( (var (make_stn 2 0 (idpath true))); (var (make_stn 2 1 (idpath true))) )]) )]) = subst compose_λ (weqvecfun 2 [( subst I1_λ (weqvecfun 0 [()]); (var (make_stn 2 1 (idpath true))) )]).
proof: Proof. unfold F_λ, term_2_λ, compose_λ, I1_λ. do 6 rewrite subst_abs. rewrite subst_var. do 9 rewrite subst_app. do 2 rewrite subst_abs. do 12 rewrite subst_var. extend_tuple_4. extend_tuple_3. extend_tuple_3. extend_tuple_3. extend_tuple_3_2. extend_tuple_1. cbn -[stnweq]. do 5 rewrite inflate_var. do 3 rewrite inflate_abs. do 3 rewrite beta_equality. rewrite subst_var. do 2 rewrite subst_app. do 6 rewrite subst_abs. do 3 rewrite subst_subst. rewrite extend_tuple_inr. do 3 rewrite subst_var. do 4 rewrite subst_app. do 3 rewrite extend_tuple_inr. do 6 rewrite subst_var. do 5 rewrite extend_tuple_inl. do 4 rewrite extend_tuple_inr. rewrite subst_var. do 7 rewrite inflate_var. rewrite beta_equality. rewrite extend_tuple_inr. do 3 rewrite subst_var. do 4 rewrite subst_app. do 5 rewrite extend_tuple_inl. rewrite extend_tuple_inr. rewrite subst_var. do 3 rewrite inflate_var. rewrite extend_tuple_inr. do 3 rewrite subst_var. rewrite beta_equality. do 3 rewrite extend_tuple_inl. rewrite subst_abs. rewrite beta_equality. 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