fact: Definition inflate_var {L : lambda_calculus_data} {n} (i : stn n) : inflate (L := L) (var i) = var (stnweq (inl i)) := subst_var i _.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Tuples