Add hints to the NotIntro levels

[mcol]

I'm finding these levels really hard, although up to here I've been doing ok. As these levels rely on writing lambdas that get each time more complicated, it would be helpful to have more optional hints of the form:

Begin with λ(nsc : ¬S ∧ C) ↦

as this would allow some more progress.

[Trequetrum]

You're right. I think the learning curve on implications can be smoothed out across a few of the worlds a bit better.