-/2 width=3/ qed-.
-
-fact ssta_inv_gref1_aux: ∀h,g,L,T,U,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l, U⦄ → ∀p0. T = §p0 → ⊥.
-#h #g #L #T #U #l * -L -T -U -l
-[ #L #k #l #_ #p0 #H destruct
-| #L #K #V #W #U #i #l #_ #_ #_ #p0 #H destruct
-| #L #K #W #V #U #i #l #_ #_ #_ #p0 #H destruct
-| #a #I #L #V #T #U #l #_ #p0 #H destruct
-| #L #V #T #U #l #_ #p0 #H destruct
-| #L #W #T #U #l #_ #p0 #H destruct
-qed.
-
-lemma ssta_inv_gref1: ∀h,g,L,U,p,l. ⦃G, L⦄ ⊢ §p •[h, g] ⦃l, U⦄ → ⊥.
-/2 width=9/ qed-.
-
-fact ssta_inv_bind1_aux: ∀h,g,L,T,U,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l, U⦄ →
- ∀a,I,X,Y. T = ⓑ{a,I}Y.X →
- ∃∃Z. ⦃h, L.ⓑ{I}Y⦄ ⊢ X •[h, g] ⦃l, Z⦄ & U = ⓑ{a,I}Y.Z.
-#h #g #L #T #U #l * -L -T -U -l
-[ #L #k #l #_ #a #I #X #Y #H destruct
-| #L #K #V #W #U #i #l #_ #_ #_ #a #I #X #Y #H destruct
-| #L #K #W #V #U #i #l #_ #_ #_ #a #I #X #Y #H destruct
-| #b #J #L #V #T #U #l #HTU #a #I #X #Y #H destruct /2 width=3/
-| #L #V #T #U #l #_ #a #I #X #Y #H destruct
-| #L #W #T #U #l #_ #a #I #X #Y #H destruct
+/2 width=3 by ssta_inv_lref1_aux/ qed-.
+
+fact ssta_inv_gref1_aux: ∀h,g,G,L,T,U. ⦃G, L⦄ ⊢ T •[h, g] U → ∀p0. T = §p0 → ⊥.
+#h #g #G #L #T #U * -G -L -T -U
+[ #G #L #k #p0 #H destruct
+| #G #L #K #V #U #W #i #_ #_ #_ #p0 #H destruct
+| #G #L #K #W #U #l #i #_ #_ #_ #p0 #H destruct
+| #a #I #G #L #V #T #U #_ #p0 #H destruct
+| #G #L #V #T #U #_ #p0 #H destruct
+| #G #L #W #T #U #_ #p0 #H destruct
+]
+qed-.
+
+lemma ssta_inv_gref1: ∀h,g,G,L,U,p. ⦃G, L⦄ ⊢ §p •[h, g] U → ⊥.
+/2 width=9 by ssta_inv_gref1_aux/ qed-.
+
+fact ssta_inv_bind1_aux: ∀h,g,G,L,T,U. ⦃G, L⦄ ⊢ T •[h, g] U →
+ ∀b,J,X,Y. T = ⓑ{b,J}Y.X →
+ ∃∃Z. ⦃G, L.ⓑ{J}Y⦄ ⊢ X •[h, g] Z & U = ⓑ{b,J}Y.Z.
+#h #g #G #L #T #U * -G -L -T -U
+[ #G #L #k #b #J #X #Y #H destruct
+| #G #L #K #V #U #W #i #_ #_ #_ #b #J #X #Y #H destruct
+| #G #L #K #W #U #l #i #_ #_ #_ #b #J #X #Y #H destruct
+| #a #I #G #L #V #T #U #HTU #b #J #X #Y #H destruct /2 width=3/
+| #G #L #V #T #U #_ #b #J #X #Y #H destruct
+| #G #L #W #T #U #_ #b #J #X #Y #H destruct
+]
+qed-.
+
+lemma ssta_inv_bind1: ∀h,g,b,J,G,L,Y,X,U. ⦃G, L⦄ ⊢ ⓑ{b,J}Y.X •[h, g] U →
+ ∃∃Z. ⦃G, L.ⓑ{J}Y⦄ ⊢ X •[h, g] Z & U = ⓑ{b,J}Y.Z.
+/2 width=3 by ssta_inv_bind1_aux/ qed-.
+
+fact ssta_inv_appl1_aux: ∀h,g,G,L,T,U. ⦃G, L⦄ ⊢ T •[h, g] U → ∀X,Y. T = ⓐY.X →
+ ∃∃Z. ⦃G, L⦄ ⊢ X •[h, g] Z & U = ⓐY.Z.
+#h #g #G #L #T #U * -G -L -T -U
+[ #G #L #k #X #Y #H destruct
+| #G #L #K #V #U #W #i #_ #_ #_ #X #Y #H destruct
+| #G #L #K #W #U #l #i #_ #_ #_ #X #Y #H destruct
+| #a #I #G #L #V #T #U #_ #X #Y #H destruct
+| #G #L #V #T #U #HTU #X #Y #H destruct /2 width=3/
+| #G #L #W #T #U #_ #X #Y #H destruct
+]
+qed-.
+
+lemma ssta_inv_appl1: ∀h,g,G,L,Y,X,U. ⦃G, L⦄ ⊢ ⓐY.X •[h, g] U →
+ ∃∃Z. ⦃G, L⦄ ⊢ X •[h, g] Z & U = ⓐY.Z.
+/2 width=3 by ssta_inv_appl1_aux/ qed-.
+
+fact ssta_inv_cast1_aux: ∀h,g,G,L,T,U. ⦃G, L⦄ ⊢ T •[h, g] U → ∀X,Y. T = ⓝY.X →
+ ⦃G, L⦄ ⊢ X •[h, g] U.
+#h #g #G #L #T #U * -G -L -T -U
+[ #G #L #k #X #Y #H destruct
+| #G #L #K #V #U #W #i #_ #_ #_ #X #Y #H destruct
+| #G #L #K #W #U #l #i #_ #_ #_ #X #Y #H destruct
+| #a #I #G #L #V #T #U #_ #X #Y #H destruct
+| #G #L #V #T #U #_ #X #Y #H destruct
+| #G #L #W #T #U #HTU #X #Y #H destruct //