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


            
            replaceLocalDeclInstantiateMVars.lean:54:18-57:44: error: unsolved goals

            
            h₂ : Nat

            
            h₁ : h₂ = h₂

            
            ⊢ True
	replaceLocalDeclInstantiateMVars.lean:54:18-57:44: error: unsolved goals
	h₂ : Nat
	h₁ : h₂ = h₂
	⊢ True