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


            
            x x✝ y : Nat

            
            h : g x = y.succ

            
            ⊢ g x = 2 * x + 1