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 beqid. 도 마찬가지입니다. 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]

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