proposition: Lemma term_1_compose_2_λ : subst term_1_λ (weqvecfun 1 [(subst compose_2_λ (weqvecfun 3 [(subst compose_λ (weqvecfun 2 [(subst I2_λ (weqvecfun 0 [()]); (var (make_stn 1 0 (idpath true))))]); subst (T_λ) (weqvecfun 0 [()]); subst (F_λ) (weqvecfun 0 [()]))]))]) = subst compose_λ (weqvecfun 2 [(subst I2_λ (weqvecfun 0 [()]); (var (make_stn 1 0 (idpath true))))]).
proof: Proof. unfold term_1_λ, compose_2_λ. do 3 rewrite subst_abs. do 5 rewrite subst_app. rewrite subst_abs. do 5 rewrite subst_var. do 2 rewrite subst_app. do 3 rewrite subst_var. extend_tuple_4. extend_tuple_4_1. extend_tuple_4_2. extend_tuple_4_3. extend_tuple_3. extend_tuple_2. set (a := weqvecfun 2 [(_ ; _)]). cbn -[a stnweq]. unfold inflate. do 3 rewrite subst_var. do 2 rewrite subst_abs. do 4 rewrite subst_subst. rewrite beta_equality. do 8 rewrite subst_app. do 7 rewrite subst_subst. rewrite subst_var. rewrite subst_subst. rewrite extend_tuple_inr. rewrite subst_var. rewrite extend_tuple_inr. rewrite subst_var. rewrite extend_tuple_inr. rewrite (iscontr_uniqueness (iscontr_empty_tuple (lambda 3)) _). unfold compose_λ. do 2 rewrite subst_abs. rewrite beta_equality. do 6 rewrite subst_app. do 3 rewrite subst_subst. do 6 rewrite subst_var. extend_tuple_3. extend_tuple_3. cbn -[stnweq]. do 3 rewrite subst_var. do 3 rewrite subst_subst. rewrite inflate_var. rewrite extend_tuple_inl. rewrite extend_tuple_inr. rewrite inflate_var. rewrite subst_var. rewrite extend_tuple_inl. rewrite inflate_var. rewrite subst_var. rewrite extend_tuple_inl. rewrite inflate_var. rewrite subst_var. rewrite extend_tuple_inl. unfold inflate. do 3 rewrite subst_subst. rewrite (iscontr_uniqueness (iscontr_empty_tuple (lambda 3)) _). unfold I2_λ. do 4 rewrite subst_abs. do 2 rewrite beta_equality. do 2 rewrite subst_app. do 2 rewrite subst_abs. rewrite beta_equality. do 4 rewrite subst_var. do 3 rewrite subst_app. do 2 rewrite subst_subst. extend_tuple_2. extend_tuple_1. unfold inflate. do 3 rewrite subst_var. rewrite extend_tuple_inl. do 2 rewrite extend_tuple_inr. rewrite subst_var. do 4 rewrite subst_app. do 2 rewrite subst_abs. do 4 rewrite subst_subst. rewrite extend_tuple_inr. do 2 rewrite subst_var. do 2 rewrite subst_app. rewrite extend_tuple_inl. do 3 rewrite subst_var. do 2 rewrite extend_tuple_inl. rewrite extend_tuple_inr. rewrite subst_var. do 2 rewrite inflate_var. rewrite extend_tuple_inr. do 2 rewrite subst_var. do 4 rewrite extend_tuple_inl. do 2 rewrite inflate_var. rewrite (iscontr_uniqueness (iscontr_empty_tuple (lambda 3)) _). unfold T_λ, F_λ. do 2 rewrite subst_abs. do 2 rewrite beta_equality. do 4 rewrite subst_app. do 8 rewrite subst_abs. do 4 rewrite subst_subst. do 4 rewrite subst_var. extend_tuple_3_1. extend_tuple_3_2. extend_tuple_2. extend_tuple_2_1. extend_tuple_1. extend_tuple_1. extend_tuple_1. do 6 rewrite subst_var. rewrite inflate_var. rewrite extend_tuple_inl. do 5 rewrite extend_tuple_inr. rewrite subst_var. rewrite subst_app. do 2 rewrite beta_equality. rewrite extend_tuple_inl. rewrite extend_tuple_inr. do 2 rewrite subst_var. do 4 rewrite subst_app. rewrite inflate_var. do 6 rewrite subst_var. do 4 rewrite extend_tuple_inl. do 2 rewrite extend_tuple_inr. do 2 rewrite beta_equality. do 2 rewrite subst_abs. do 2 rewrite beta_equality. do 2 rewrite subst_var. rewrite extend_tuple_inl. do 2 rewrite extend_tuple_inr. rewrite subst_var. rewrite inflate_var. rewrite extend_tuple_inr. rewrite subst_var. now rewrite extend_tuple_inl. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.Tuples UniMath.Combinatorics.Vectors UniMath.Combinatorics.StandardFiniteSets UniMath.AlgebraicTheories.LambdaCalculus