proposition: Lemma compose_assoc_λ (n : nat) (i j k : stn n) : subst compose_λ (weqvecfun 2 [( subst compose_λ (weqvecfun 2 [( var i ; var j )]) ; var k)]) = subst compose_λ (weqvecfun 2 [( var i ; subst compose_λ (weqvecfun 2 [( var j ; var k )]) )]).
proof: Proof. unfold compose_λ. cbn -[weqvecfun]. refine (maponpaths (λ x, subst _ (weqvecfun _ [(x ; _)])) (subst_abs _ _) @ _). refine (compose_abs_λ _ _ _ @ _). do 4 rewrite subst_app. do 2 rewrite subst_abs. do 3 rewrite subst_subst. rewrite inflate_var. do 3 rewrite subst_var. do 4 rewrite subst_app. do 6 rewrite subst_var. apply maponpaths. extend_tuple_3. cbn -[stnweq weqvecfun extend_tuple]. rewrite subst_var. rewrite extend_tuple_inr. do 2 extend_tuple_3. cbn -[stnweq]. do 3 rewrite inflate_var. rewrite inflate_abs. rewrite beta_equality. do 2 rewrite subst_var. do 4 rewrite subst_app. do 3 rewrite subst_subst. do 2 rewrite extend_tuple_inl. do 3 rewrite subst_var. do 2 rewrite extend_tuple_inl. rewrite extend_tuple_inr. rewrite subst_var. do 4 rewrite inflate_var. rewrite extend_tuple_inr. do 2 rewrite subst_var. now do 2 rewrite extend_tuple_inl. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.Tuples UniMath.Combinatorics.Vectors UniMath.Combinatorics.StandardFiniteSets UniMath.AlgebraicTheories.LambdaCalculus