(* Properties with contextual transitive closure ****************************)
lemma lprs_CTC (h) (G):
- â\88\80L1,L2. L1⪤[CTC â\80¦ (λL. cpm h G L 0)] L2 â\86\92 â\9dªG,L1â\9d«⊢ ➡*[h,0] L2.
+ â\88\80L1,L2. L1⪤[CTC â\80¦ (λL. cpm h G L 0)] L2 â\86\92 â\9d¨G,L1â\9d©⊢ ➡*[h,0] L2.
/3 width=3 by cprs_CTC, lex_co/ qed.
(* Inversion lemmas with contextual transitive closure **********************)
lemma lprs_inv_CTC (h) (G):
- â\88\80L1,L2. â\9dªG,L1â\9d«⊢ ➡*[h,0] L2 → L1⪤[CTC … (λL. cpm h G L 0)] L2.
+ â\88\80L1,L2. â\9d¨G,L1â\9d©⊢ ➡*[h,0] L2 → L1⪤[CTC … (λL. cpm h G L 0)] L2.
/3 width=3 by cprs_inv_CTC, lex_co/ qed-.