Let's think about one more strategy example. Like the last, we need to set ourselves up by first providing the appropriate input.

Start the demonstration...

MouseOver the sign to pause
the demonstration

 

Replay the demonstration.
Next...

Line 2 says that at least one thing is an M...we assume that 't' names such an individual.

Because we are looking forward to using %E, we have a new goal: to derive (%y)Byc by line 6 at the end of the subderivation.

Now that we know where we need to "go" (to subderive line 6) the derivation is fairly easy...

Finally, we have the two ingredients needed as input for %E: the existential statement on line 2 (green) and the appropriate subderivation (blue).