-lemma tsts_inv_pair2: ∀I,T1,W2,U2. T1 ≂ ②{I}W2.U2 →
- ∃∃W1,U1. T1 = ②{I}W1.U1.
-/2 width=5 by tsts_inv_pair2_aux/ qed-.
+(* Basic_1: was: iso_gen_head *)
+lemma tsts_inv_pair1: ∀h,o,J,W1,U1,T2. ②{J}W1.U1 ⩳[h, o] T2 →
+ ∃∃W2,U2. T2 = ②{J}W2. U2.
+/2 width=7 by tsts_inv_pair1_aux/ qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma tsts_inv_sort1_deg: ∀h,o,Y,s1. ⋆s1 ⩳[h, o] Y → ∀d. deg h o s1 d →
+ ∃∃s2. deg h o s2 d & Y = ⋆s2.
+#h #o #Y #s1 #H #d #Hs1 elim (tsts_inv_sort1 … H) -H
+#s2 #x #Hx <(deg_mono h o … Hx … Hs1) -s1 -d /2 width=3 by ex2_intro/
+qed-.
+
+lemma tsts_inv_sort_deg: ∀h,o,s1,s2. ⋆s1 ⩳[h, o] ⋆s2 →
+ ∀d1,d2. deg h o s1 d1 → deg h o s2 d2 →
+ d1 = d2.
+#h #o #s1 #y #H #d1 #d2 #Hs1 #Hy
+elim (tsts_inv_sort1_deg … H … Hs1) -s1 #s2 #Hs2 #H destruct
+<(deg_mono h o … Hy … Hs2) -s2 -d1 //
+qed-.
+
+lemma tsts_inv_pair: ∀h,o,I1,I2,V1,V2,T1,T2. ②{I1}V1.T1 ⩳[h, o] ②{I2}V2.T2 →
+ I1 = I2.
+#h #o #I1 #I2 #V1 #V2 #T1 #T2 #H elim (tsts_inv_pair1 … H) -H
+#V0 #T0 #H destruct //
+qed-.