fact: Definition beta_equality {L : lambda_calculus_data} {n} (f : L (S n)) g : app (abs f) g = subst f (extend_tuple var g) := pr1 (pr222 (pr222 (pr222 L))) n f g.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Tuples