(* Properties with context-sensitive parallel eta-conversion for terms ******)
-lemma cpce_total_cnv (h) (a) (G) (L):
+axiom cpce_total_cnv (h) (a) (G) (L):
∀T1. ⦃G,L⦄ ⊢ T1 ![h,a] → ∃T2. ⦃G,L⦄ ⊢ T1 ⬌η[h] T2.
+(*
#h #a #G #L #T1 #HT1
lapply (cnv_fwd_csx … HT1) #H
generalize in match HT1; -HT1
/3 width=2 by cpce_flat, ex_intro/
]
qed-.
+*)