The standard notation for sucg a “meaning-of” operator is a pair of denotation or Scott brackets.
2.6.2.3
Might be helpful to first show the proof without the repeat and then show how long it is followed by showing how using repeat makes it much shorter. That would likely help student s get a better sense of why repeat is useful here and what is going on in the proof here as they can't step through each loop of the repeat
2.6.2.1
Typo here with "sucg" instead of "such"
2.6.2.3
Might be helpful to first show the proof without the
repeatand then show how long it is followed by showing how usingrepeatmakes it much shorter. That would likely help student s get a better sense of whyrepeatis useful here and what is going on in the proof here as they can't step through each loop of the repeat