continuation_rename is defined.
continuation_rename is defined.
Getting rid of admitted proofs.
Big ugly proof for app_produces_vvar.
Simplification, simplification, simplification.
Proof completed.