1576.lean:1:35-1:38: error(lean.unknownIdentifier): Unknown identifier `non`
1576.lean:1:41-1:46: error(lean.unknownIdentifier): Unknown identifier `sense`
1576.lean:1:18-1:50: error: unsolved goals
⊢ True