The study tasks show three headline frames for one idea:

• X is not a subtype of Y: refinement errors (A2_10, both practice tasks);
• expected Y but could not prove it: an empty Found (A2_04, A1_56);
• found X but expected Y: state errors (A1_38, A1_01, A1_09).

"is not a subtype of" is jargon, and the practice tasks teach a frame that the state tasks never use.

Proposal

Use found %s but expected %s for refinement errors as well (RefinementError). Keep expected … but could not prove it for an empty Found.

After the release, the study env must re-run the practice outputs and the tour screenshots.

An Expected-first headline (<call> needs <Expected>) is deferred until after the study.