agda: try and give up proving lift-term-doWeakenOne-ignore
agda: try and give up proving lift-term-doWeakenOne-ignore

See comments in the proof. Tillmann plans to rewrite the whole
handling of contexts.

Old-commit-hash: c120bb673f9dc0bbb6bdf96a9f0756063f874702

inc-lc/ilc-agda