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 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).