fun (A : Type.{l_1}), A : Type.{l_1} -> Type.{l_1}
fun (A : Type.{l_1}), A : Type.{l_1} -> Type.{l_1}
done