Sketch fundamental theorem with big-step semantics
Sketch fundamental theorem with big-step semantics

OK, honestly that was much easier than with functional big-step semantics.
Though probably a clever strategy would simplify those functional proofs.

Beware I haven't proven any lemmas about the semantics (other than a decider
based on the evaluator).

Also missing: lots of inequalities about step-indexes differences. Proving them
in Agda is a pain. But they all look true.

inc-lc/ilc-agda