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