+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 -T1;
+ elim (simple_inv_bind … HT1)
+| #V2 #V #W1 #W2 #U1 #U2 #_ #_ #_ #_ #H #_ destruct -T1;
+ elim (simple_inv_bind … HT1)
+]
+qed-.