Maps.beq / Datatypes.true

[9lung]

p02를 풀다가
X : Type
v1, v2 : X
x1, x2 : id
m : total_map X
H : x2 <> x1
x : id
eq1 : beq_id x1 x = true
eq2 : beq_id x2 x = true 이 상황에서

rewrite beq_id_true_iff in eq1.를 하려하니까

Error:
Found no subterm matching
"Maps.beq_id ?i ?i0 =
Datatypes.true" in the current goal. 가 뜹니다.

그리고 이 상황에서 SearchAbout beq_id_true_iff. 를 치면 아무것도 안나옵니다. SearchAbout beq_id. 도 마찬가지입니다. SearchAbout _. 을 해봤는데 beq_id에 대한 내용은 전무합니다. make도 실행한 상태입니다. 무엇이 문제인가요?

[aqjune]

@jeehoonkang 이 남긴 코멘트에 추가해서, Check beq_id_true_iff를 사용하면 어떤 결과가 나오는지도 알고 싶습니다.
일단은 급한 대로 직접 lemma를 만들어서 진행해 주세요. 폴더 내의 Maps.v에 beq_id_true_iff 의 증명이 있습니다.

[9lung]

beq_id_true_iff
: forall id1 id2 : Maps.id,
Maps.beq_id id1 id2 = Datatypes.true <-> id1 = id2

이런식으로 뜹니다. Require Export Maps를 하면 오류가 없어져서 require문을 넣고 진행했는데 문제 없겠지요?

[aqjune]

예 아마 문제없을 것 같은데, 혹시나 하니까 꼭 채점서버에서 돌려보시기 바랍니다.