+qed-.
+
+(* Note: the main property of simple terms *)
+lemma tpr_inv_appl1_simple: โV1,T1,U. ๐{Appl} V1. T1 โ U โ ๐[T1] โ
+ โโV2,T2. V1 โ V2 & T1 โ T2 &
+ U = ๐{Appl} V2. T2.
+#V1 #T1 #U #H #HT1
+elim (tpr_inv_appl1 โฆ H) -H *
+[ /2 width=5/
+| #V2 #W #W1 #W2 #_ #_ #H #_ destruct
+ elim (simple_inv_bind โฆ HT1)
+| #V2 #V #W1 #W2 #U1 #U2 #_ #_ #_ #_ #H #_ destruct
+ elim (simple_inv_bind โฆ HT1)
+]
+qed-.