agda: prove completely that diff-is-valid (#33)
agda: prove completely that diff-is-valid (#33)

The proof is much more different from the one of derive-is-valid than
I'd have expected, but it was relatively easy to complete directly in
Agda, without doing it on paper beforehand.

derive-is-valid is proved as a corollary in one line.

Old-commit-hash: fd47a2b1346fb45e5e94db8d814e83e9fdf1442d

inc-lc/ilc-agda