Take the rule for λ (simplified):
```
x:X, y:Y ⊢ z : Z
-----------------------
x:X ⊢ λ(y: Y). z : Y → Z
```

You interpret it as a statement
```
∀ v⊩A, (∀ w ⊩ B, u[x\v, y\w] ⊩ C) ⟹ \lambda y.u[x\v] ⊩ C
```

- Then, you prove this statement. 7/10

Once you've done so for each rule, you can conclude (very easy induction) that
if ⊢ u : A, then u ⊩ A. This gives type safety, since realisers are practically
defined as verifying type safety.
What you've gained along the way is that this proof is an open induction. 8/10
In standard combinatorial proofs of type safety, the induction hypothesis may
depend on every case. Adding a form in your language may require redoing the
entire proof. Here the various case in the adequacy lemma will remain true. So
you can just prove the new cases. 9/10
There are many variants of realisability. Tuned for logic, with models instead
of terms, … My favourite is Krivine's realisability with both terms and stacks,
and magic happening when they interact. But this is another story and shall be
told another time. 10/10