+fact thom_inv_bind1_aux: โT1,T2. T1 โ T2 โ โI,W1,U1. T1 = โ{I}W1.U1 โ
+ โโW2,U2. I = Abst & T2 = โW2. U2.
+#T1 #T2 * -T1 -T2
+[ #J #I #W1 #U1 #H destruct
+| #V1 #V2 #T1 #T2 #I #W1 #U1 #H destruct /2 width=3/
+| #V1 #V2 #T1 #T2 #H_ #_ #_ #I #W1 #U1 #H destruct
+]
+qed.
+
+lemma thom_inv_bind1: โI,W1,U1,T2. โ{I}W1.U1 โ T2 โ
+ โโW2,U2. I = Abst & T2 = โW2. U2.
+/2 width=5/ qed-.
+
+fact thom_inv_flat1_aux: โT1,T2. T1 โ T2 โ โI,W1,U1. T1 = โ{I}W1.U1 โ
+ โโW2,U2. U1 โ U2 & ๐[U1] & ๐[U2] &
+ I = Appl & T2 = โW2. U2.
+#T1 #T2 * -T1 -T2
+[ #J #I #W1 #U1 #H destruct
+| #V1 #V2 #T1 #T2 #I #W1 #U1 #H destruct
+| #V1 #V2 #T1 #T2 #HT12 #HT1 #HT2 #I #W1 #U1 #H destruct /2 width=5/
+]
+qed.
+
+lemma thom_inv_flat1: โI,W1,U1,T2. โ{I}W1.U1 โ T2 โ
+ โโW2,U2. U1 โ U2 & ๐[U1] & ๐[U2] &
+ I = Appl & T2 = โW2. U2.
+/2 width=4/ qed-.