-definition g := λn,m.λx:A n.b m.
-definition foo2 := λn,n1,m,m1.(g n m : A1 n1 -> B1 m1).
-definition foo3 := λn1,n,m,m1.(g n m : A1 n1 -> B1 m1).
-definition foo4 := λn1,n,m1,m.(g n m : A1 n1 -> B1 m1).
-
+definition h := λn,m.λx:A n.g m.
+definition foo2 := λn,n1,m,m1.(h n m : A1 n1 -> B1 m1).
+definition foo3 := λn1,n,m,m1.(h n m : A1 n1 -> B1 m1).
+definition foo4 := λn1,n,m1,m.(h n m : A1 n1 -> B1 m1).