Post #2141599

@ProfKinyon The Lean 4 version of the game had `apply ... at` which was missing in Lean 3. All of the function and proposition world thing was to really try and explain that logical implication can be thought of as a function, and all of that was an attempt to make students understand how `apply f` could turn the target of `f` into its source and thus argue in a direction which they don't normally think about. In the Lean 4 version I have dumped this completely, there are no abstract propositions at all, it's all numbers, and we can argue the normal way (forwards) with `apply at` and it's much easier.