[질문] 이거 Idris에서 증명가능함 ㅇㅅㅇ?

[기괴공학도(mecheng98)]

runEqn : x = y → P x x → P x y

- dc official App

[다믜(damhiya)]

ㅇㅇ 가능

[기괴공학도(mecheng98)]

그냥 바로 생각나는 게 정답이죠? - dc App

[다믜(damhiya)]

runEqn e p = replace {P=P x} e p 라고 하면 될것 같은데

[기괴공학도(mecheng98)]

아 ㄱㅅㄱㅅ - dc App

[다믜(damhiya)]

runEqn Refl p = p 도 될것 같은데

[기괴공학도(mecheng98)]

바로 생각나는 게 이걸 말하는 거였어요 ㅇㅅㅇ - dc App

[다믜(damhiya)]

쌉고수

[기괴공학도(mecheng98)]

님이 더;; - dc App