proposition: Lemma compose_abs_λ (n : nat) (a : lambda (S n)) (b : lambda n) : subst compose_λ (weqvecfun 2 [(abs a ; b)]) = (abs (subst a (extend_tuple (λ i, var (stnweq (inl i))) (app (inflate b) (var (stnweq (inr tt))))))).
proof: Proof. unfold compose_λ. rewrite subst_abs. do 2 rewrite subst_app. do 3 rewrite subst_var. extend_tuple_3. cbn -[stnweq]. apply maponpaths. rewrite inflate_abs. rewrite beta_equality. rewrite subst_subst. apply maponpaths. apply funextfun. intro i. rewrite <- (homotweqinvweq stnweq i). induction (invmap stnweq i); refine (maponpaths (λ x, subst (_ x) _) (homotinvweqweq stnweq _) @ !_); refine (maponpaths _ (homotinvweqweq stnweq _) @ !_); cbn -[stnweq]. - do 2 rewrite inflate_var. rewrite subst_var. now rewrite extend_tuple_inl. - 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