Qcert.Translation.TNRAtocNNRC
Type preservation for the translation from NRA to NNRC
Context {m:basic_model}.
Theorem tnra_sem_correct {τin τout} (op:nra) (tenv:tbindings) (v:var) :
(op ▷ τin >=> τout) →
lookup equiv_dec tenv v = Some τin →
nnrc_type tenv (nra_to_nnrc op v) τout.
Reverse direction, main theorem
Theorem tnra_sem_correct_back {τin τout} (op:nra) (tenv:tbindings) (v:var) :
nnrc_type tenv (nra_to_nnrc op v) τout →
lookup equiv_dec tenv v = Some τin →
(op ▷ τin >=> τout).
Theorem 7.4: NRA<->NNRC.
Final iff Theorem of type preservation for the translation from NRA to NNRC