fact: Definition F_λ : lambda 0 := abs (app (var (make_stn 1 0 (idpath true))) (abs (abs (var (make_stn 3 2 (idpath true)))))).
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.Tuples UniMath.Combinatorics.Vectors UniMath.Combinatorics.StandardFiniteSets UniMath.AlgebraicTheories.LambdaCalculus