destruct n as [|n'] eqn : E.
여기서 eqn 자리에는 다른 것들이 올 수 있나요?
예를 들어 목표가 부등식이라면 뭐가 오나요?

- dc official App