proposition: Lemma subst_l_var {L : lambda_calculus} {n : nat} (l : L n) : subst l var = l.
proof: Proof. use (lambda_calculus_ind_prop (λ n l, (subst l var = l) ,, (setproperty _ _ _))); cbn. - intros. apply subst_var. - intros ? ? ? H1 H2. now rewrite subst_app, H1, H2. - intros ? ? H. rewrite subst_abs. apply maponpaths. refine (_ @ H). apply maponpaths. apply extend_tuple_eq. + intro. apply inflate_var. + apply idpath. - intros ? ? ? ? ? H. rewrite subst_subst. apply maponpaths. apply funextfun. intro. apply H. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Tuples