fact: Definition var {L : lambda_calculus_data} {n : nat} (i : stn n) : L n := pr12 L n i.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Tuples