proposition: Lemma subst_inflate {L : lambda_calculus_data} {m n} (l : L m) (f : stn (S m) → L n) : subst (inflate l) f = subst l (λ i, f (stnweq (inl i))).
proof: Proof. unfold inflate. rewrite subst_subst. apply maponpaths. apply funextfun. intro i. now rewrite subst_var. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Tuples