fact: Definition app {L : lambda_calculus_data} {n : nat} (l l' : L n) : L n := pr122 L n l l'.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Tuples