agda: we don't need a proof that the input change is valid (#33)
agda: we don't need a proof that the input change is valid (#33)

diff is defined on the semantic domain, so it produces a valid change
on functions even when the input is not a valid change (maybe this
extends to the syntactic domain, but I won't claim that).

However, the proof of correctness of symbolic derivation uses
diff-apply, which is still only valid on valid changes, as visible in
the type of diff-apply-proof.

Currently, diff-is-valid and derive-is-valid are unused. However, when
the proof of derive-term will use diff-apply-proof, derive-term will
only be valid on valid changes; so diff-is-valid and derive-is-valid
will be required to prove that we can produce such valid changes.

Additionally, remark that now validity proofs form a strictly positive
datatype, so they could be encoded with a standard datatype.

Moreover, validity proofs are not any more a logical relation.

Old-commit-hash: 1a3d91d1304701dead9c75f987d7e19b4fb45401

inc-lc/ilc-agda