Solution to 7.1 is not fair, based on unlock from 6.2

[misterbeebee]

DOUBLE DEDUCTION THEOREM Is unlocked by solving 6.2, and 7.1 shortest proof uses DDT, but exercise 7.1 is not dependent on 6.2 for unlock.

Therefore, the shortest solution is impossible for players who jump from 6.1 to 7.1, and the UI gives no indication of why.

Either DDT should be unlocked (silently) by 6.1, or 7.1 should be unlocked by 6.2 instead of 6.1(a)

<div class="exercise" id="EXERCISE-7.1" data-unlocked-by="6.1(a)" data-unlocks="Push PushAlt">
        </div>
        <ol class="proof">
            <li><span>Deduce <em>A</em> [assuming <em>A</em>]. <i>[IMPLICATION INTRODUCTION]</i></span></li>
            <li><span>From <em>A</em> [assuming <em>A</em>]: deduce <em>A</em> [assuming <em>A</em>, <em>B</em>]. <i>[PUSH (alternate form)]</i></span></li>
            <li><span>From <em>A</em> [assuming <em>A</em>, <em>B</em>]: deduce <em>A</em> IMPLIES (<em>B</em> IMPLIES <em>A</em>). <i>[DOUBLE <a href="https://en.wikipedia.org/wiki/Deduction_theorem" target="_blank">DEDUCTION THEOREM</a>]</i></span></li>
            <li><span>QED!</span></li>

[misterbeebee]

Also, and compounding thebconfusion, for solvers of 7.2, it is very hard to distinguish PUSH and PUSH-ALT when using a touchscreen, since the hitboxes are invisible and very close together.

It might help to make PUSH and PUSH-ALT explicitly named in the instructions as separate operations. Currently, the "Alternately,...." text makes it seem like PUSH-ALT is just a different way to draw PUSH, but really it is a double operation ASSUME+PUSH so should be documented as such.
Maybe even try to prevent the confusion, by changing and adding an exercise to introduce PUSH-ALT separately, after a first PUSH exercise.

[misterbeebee]

I can’t repro the “Double Deduction Theorem not available” now, even though I was able to repro earlier.
Maybe it’s just the touchscreen experience on iPad makes precise dragging hard, or maybe there is some state in my browser making me unable to re-lock the Double Decuction Theorem.