|
|
|
|
|
|
by marktani
26 days ago
|
|
|
I sort of reverse engineered the first couple riddles (the help menu helped too) before really getting the logic here. What I gathered: - the paramaeters in lemma banish() are "given"
- the statement right after lemma banish() is what we want to prove
- all "wip" needs to replaced by something
- blocks need to be finished with "qed;" From there it's using the available tools. |
|
|