fact: Definition inflate_app {L : lambda_calculus_data} {n} (l l' : L n) : inflate (L := L) (app l l') = app (inflate l) (inflate l') := subst_app l l' _.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Tuples