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


          
            
            example (a : α) : ¬ some (some a) = some none := by simp