(* *)
(**************************************************************************)
-include "ground_2/xoa/ex_7_5.ma".
+include "ground/xoa/ex_7_5.ma".
include "basic_2/rt_equivalence/cpcs_cprs.ma".
include "basic_2/dynamic/cnv_preserve.ma".
include "basic_2/i_dynamic/ntas.ma".
(* Properties based on preservation *****************************************)
lemma cnv_cpms_ntas (h) (a) (G) (L):
- ∀T. ❪G,L❫ ⊢ T ![h,a] → ∀n,U.❪G,L❫ ⊢ T ➡*[n,h] U → ❪G,L❫ ⊢ T :*[h,a,n] U.
+ ∀T. ❪G,L❫ ⊢ T ![h,a] → ∀n,U.❪G,L❫ ⊢ T ➡*[h,n] U → ❪G,L❫ ⊢ T :*[h,a,n] U.
/3 width=4 by ntas_intro, cnv_cpms_trans/ qed.
(* Inversion lemmas based on preservation ***********************************)