Define translation operator; stage the proof to be bidirectional; replace correspondance between PTS's with lemmas of injective maps between sorts and axioms of CCw and Typer

Add labels and refs to equations; add (Prop, Prop, Prop) axiom to Rcc; define translation on applications; prove (most of) lemma 3.6

Finish proof of lemma 3.6; make it a case analysis on [M]* rather than [M]; make M -> M* definition a figure

Enhance layout of translation section; define soundness/completeness of translation; label lemmas; clean A-equiv lemma; add R-equiv lemma; complete completeness (=>) proof

Reduce margin; avoid undefined use of ∪ with CCω sorts; make eq:corresctness-translation a theorem; finish proof of lem:R-equiv; start proof of lem:Re-equiv

Populate soundness proof with typing rules; rephrase some sentences to be impersonal; add substitution in definition of translation

Rewrite a valid proof of lem:E-Lam-FV; start proof of soundness of translation; expand on guarded by destructors predicate D

Rephrase parts of completeness of translation proof; finish soundness of translation proof; finish example

Restructure some sentences; add recursive definition of free variables; define beta- and iota-reductions; add transitivity to congruence relation