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



            
            @[simp]

            
            theorem : True := by constructor