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 l

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.