tests/lean/binderCacheIssue2.lean.expected.out - third_party/github.com/leanprover/lean4 - Git at Google


            
            def foo.{u, u_1} : {P : Sort u} → Bar P → Type :=

            
            fun {P} B => Foo ((p : P) → Bar.fn p) ({p : P} → Bar.fn p)
	def foo.{u, u_1} : {P : Sort u} → Bar P → Type :=
	fun {P} B => Foo ((p : P) → Bar.fn p) ({p : P} → Bar.fn p)