moving forward with the proof of type safety

[vidsinghal]

Trying to prove type safety by making some assumptions explicit in the code

[ulysses4ever]

Do you think we can mark it as a draft until there's a progress in the proof that you want to merge?

[vidsinghal]

Do you think we can mark it as a draft until there's a progress in the proof that you want to merge?

yeah

[vidsinghal]

@michaelborkowski it may be useful to look at this branch since there are many more assumptions made here.

[michaelborkowski]

What is the difference with this branch? Does it have all the code removed from main?

[vidsinghal]

No it doesn't have the code removed from main but now that there is a script it can be applied on this branch too.
I've just attempted to make progress on a few more helper proofs which will help proving type safety. More assumptions that are not explicit in the Local thesis.