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