fact: Definition subst {L : lambda_calculus_data} {m n : nat} (l : L m) (f : stn m → L n) : L n := pr12 (pr222 L) m n l f.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Tuples