Every name the compiler's context has typed holds, if the environment binds it at all, a value of that type, and every name it binds is one the context has.

The second half is what a call and a function reference need. eval reads the callee out of the environment while the generated code was compiled against the context, so a name the context did not have would send the two sides to different declarations.

The expression forms type soundness reaches.

Every shape of the subset type checks. The judgement covers the syntax, so the induction it drives reads as a case analysis on the expression.

Reflexivity for the plain list comparison the entry check and the signatures use, which goes through List's own BEq rather than Ty.beqList.

A receiver a dictionary operation accepted holds exactly what the Map spelling asks for, whichever of the two the author declared. This is what lets the four cases below read either receiver through the .dict lemmas rather than through two copies of each.

Soundness of the plain list comparison, matching tyList_beq_refl.

The converse direction: a function value satisfies no type but a function type. What a call needs, since eval reads the callee out of the environment.

Reading the check element by element, so that every list operation that only ever keeps elements it was given inherits it from a membership lemma about that operation.

The count has to be the typed value rather than a bare Int: what keeps every element inside Int53 is that the count already is, and the elements are all below it.

The type the compiler gives a binary operation whose operands both have type t.

A function value in the environment is one the context typed as a function: it is bound, so the context has a type for it, and only a function type is satisfied by a function value.

Writing a key already present leaves the key list alone, and writing a new one appends a key the list did not have. Either way a Map still holds every key once.

The constructors a use of the type at args sees are the declared ones with their field types substituted, so a lookup by name lands on the same constructor either way.

A field the fold walks into is the type coming round, at the arguments the fold names. foldKindOf is read by the evaluator and by the emitter alike, so what it answers is what both walk.

Reading a field out of a value by name gives the type the declaration puts at that name. hasFieldTys lines the value's fields up with the declared ones in order, and the names being apart is what makes the lookup land on the same one.

No name the compiler lets through can be the one match gives its scrutinee: validateIdent rejects the __ prefix, and scrutName starts with it.

A call checks its arguments against the types of the callee's parameters. The names come from the same parameter list, so the check the compiler wrote over types alone reads as one over parameters.

Every argument has the type its parameter declared.

The compiler's context and the reference environment are built from the same parameter list in the same order, so the name each lookup lands on is the same one.

The arguments of a call, carrying the induction hypothesis of typeSound along them: the environment the callee's body runs in is typed by the context that body was compiled against.

What a pattern bound, against what the arm was compiled against: the same names in the same order, each value satisfying the type the compiler read.

The fields a constructor pattern reads, as the type checker sees them and as the value holds them. signature is the compiler's view of a type's constructors; Value.hasTy is the reference semantics'.

A pattern that matched bound exactly what the compiler compiled the arm against.

A fold's alternative binds what the compiler compiled its arm against. The rebuilt node carries the answer for every field that came round, so the types the binders take are foldFieldTys' and not the declared ones; everything nested inside a field reads through patPartsList unchanged.