So that was the lemma that the substitution lemma

which was necessary as we found out for solving the exercise and I sketched the

proof of that lemma on Thursday.

Yes.

So that's something that we discussed in firstly.

And I've sketched a proof.

And there were some subtleties in the proof.

And they didn't manage to fix it.

So I looked at it offline and find out what the problem was.

So the proof was by induction.

And the most interesting case was the one where q was equal to do y gets s t.

So that was the most interesting case.

And so we've calculated this two things.

So the left hand side and the right hand side.

So this side q p x.

That was calculated correctly.

So it was calculated like this.

We've got

So f is this.

And then there was h.

So it must be just t b.

And there was w.

So w was this thing.

So was it actually consistent in terms of typing?

So I think this is all right.

And then there were some problems with the right hand side.

So the right hand side was like this.

So I think this is all right.

So that's the right hand side.

That's equal to the following thing.

So that's the right hand side.

So this guys are the same.

So we found out that this is not equal to that.

And I didn't bring it to the end yet.

So there was one thing here which is a bit not very formal.

I've introduced this swap functions which rearranges the types in the context.

So I just explain it roughly how it works.

But in principle it's something that needs a proof.

But then again there was yet another thing which requires a proof.

So the mistake was that I've just replaced this by h I guess.

By no sorry this is probably not t this must be.

Something is wrong here.

So f is used twice and then there is h and this must be

this must be p right.

So the problem was that I've replaced this by f.

But now when you write down all the context you see that it's not f.

Because f depends only on gamma and this term depends on gamma and yet another variable.

So this semantics is not f.

It's f composed with the projection to gamma.

And that does the job.