qed-.
(* Note: the main property of simple terms *)
-lemma tpr_inv_appl1_simple: â\88\80V1,T1,U. â\93\90V1. T1 â\9e¡ U â\86\92 ð\9d\95\8a[T1] →
+lemma tpr_inv_appl1_simple: â\88\80V1,T1,U. â\93\90V1. T1 â\9e¡ U â\86\92 ð\9d\90\92[T1] →
∃∃V2,T2. V1 ➡ V2 & T1 ➡ T2 &
U = ⓐV2. T2.
#V1 #T1 #U #H #HT1