Added proof of interpolation lemma

[franconi]

Closes Issue #102

---

Preview | Diff

[franconi]

The proof was already discussed and approved in the associated issue #102. We need just to approve the format of the proof in the spec.

[pfps]

The technical content looks good to me. We can wrangle over the details of the wording later.

[pfps]

There is still a block on issue 102 that should be removed.

[TallTed]

I think these paragraphs would be clearer to readers — especially those unfamiliar with presentations of rigorous logic — if there were some formatting of elements like A, I, g, ∃ A . [I+A](g) = TRUE — whether that is simply <code>, <i>, <b>, or otherwise. I don't have any specific wishes nor immediate suggestions, but hope that @hartig, @doerthe, @franconi, and/or @pfps will have good ideas.

[franconi]

There is still a block on issue 102 that should be removed.

@pfps Which is it, exactly?

[franconi]

SOrry, my misunderstanding, the proof was already there, fixed by @doerthe in PR #165.
Closing this PR without committing.

[franconi]

SOrry, my misunderstanding, the proof was already there, fixed by @doerthe in PR #165.
Closing this PR without committing.