Assignment 8 Question 11, use of update_same

[AdamBJ]

Judging by the proximity of (\ *** Exercise: 2 stars (assign_aequiv) ) to the section on functional_extensionality in the textbook, I guess that we're meant to use functional_extensionality in question 11.

Indeed, I was able to use functional_extensionality to get the goal to the form st' x = update st' X (st' X) x. From here, I want to use the update_same lemma as the textbook authors did to prove the identity_assignment theorem in the The Functional Equivalence Axiom section of the text. However, since we're not given the lemma update_same in A8_00 I can't use it.

Given that this is a 2 star question, I guess we're meant to be able to use update_same as it is used in the textbook. Can it be added to Assignment8_00? Usually I'd just copy/paste the proof for update_same into the question, but update_same was proved as an exercise that we weren't assigned. If it's not possible to do this, can anyone suggest a clever workaround?

[jaewooklee93]

Well.. That proposition can be proved in one simple line.

[jeehoonkang]

Do not modify 00.v.

[PakHyungHoon]

오늘 숙제에 관련된 질문을 하러 방문해도 되나요?

[jeehoonkang]

@PakHyungHoon I will be absent today, but send me email to make an appointment.