tests/lean/autoBoundPostponeLoop.lean - third_party/github.com/leanprover/lean4 - Git at Google


            
            theorem ex

            
                 (h₁ : α = β)

            
                 (as : List α)

            
                 (bs : List β)

            
                 (h₂ : (h ▸ as) = bs)

            
                 : True :=

            
              True.intro
	theorem ex
	(h₁ : α = β)
	(as : List α)
	(bs : List β)
	(h₂ : (h ▸ as) = bs)
	: True :=
	True.intro