+fact lsubf_inv_unit2_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
+ ∀g2,I,K2. f2 = ⫯g2 → L2 = K2.ⓤ{I} →
+ ∨∨ ∃∃g1,K1. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f1 = ⫯g1 & L1 = K1.ⓤ{I}
+ | ∃∃g,g0,g1,J,K1,V. ⦃K1, g0⦄ ⫃𝐅* ⦃K2, g2⦄ &
+ K1 ⊢ 𝐅*⦃V⦄ ≡ g & g0 ⋓ g ≡ g1 & f1 = ⫯g1 &
+ L1 = K1.ⓑ{J}V.
+#f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
+[ #f1 #f2 #_ #g2 #J #K2 #_ #H destruct
+| #f1 #f2 #I1 #I2 #L1 #L2 #H12 #g2 #J #K2 #H elim (discr_push_next … H)
+| #f1 #f2 #I #L1 #L2 #H12 #g2 #J #K2 #H1 #H2 destruct
+ <(injective_next … H1) -g2 /3 width=5 by ex3_2_intro, or_introl/
+| #f #f0 #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #g2 #J #K2 #_ #H destruct
+| #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #Hf #Hf1 #H12 #g2 #J #K2 #H1 #H2 destruct
+ <(injective_next … H1) -g2 /3 width=11 by ex5_6_intro, or_intror/
+]
+qed-.
+
+lemma lsubf_inv_unit2: ∀f1,g2,I,L1,K2. ⦃L1, f1⦄ ⫃𝐅* ⦃K2.ⓤ{I}, ⫯g2⦄ →
+ ∨∨ ∃∃g1,K1. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f1 = ⫯g1 & L1 = K1.ⓤ{I}
+ | ∃∃g,g0,g1,J,K1,V. ⦃K1, g0⦄ ⫃𝐅* ⦃K2, g2⦄ &
+ K1 ⊢ 𝐅*⦃V⦄ ≡ g & g0 ⋓ g ≡ g1 & f1 = ⫯g1 &
+ L1 = K1.ⓑ{J}V.
+/2 width=5 by lsubf_inv_unit2_aux/ qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma lsubf_inv_atom: ∀f1,f2. ⦃⋆, f1⦄ ⫃𝐅* ⦃⋆, f2⦄ → f1 ≗ f2.
+#f1 #f2 #H elim (lsubf_inv_atom1 … H) -H //
+qed-.
+
+lemma lsubf_inv_push_sn: ∀g1,f2,I1,I2,K1,K2. ⦃K1.ⓘ{I1}, ↑g1⦄ ⫃𝐅* ⦃K2.ⓘ{I2}, f2⦄ →
+ ∃∃g2. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f2 = ↑g2.
+#g1 #f2 #I #K1 #K2 #X #H elim (lsubf_inv_push1 … H) -H
+#g2 #I #Y #H0 #H2 #H destruct /2 width=3 by ex2_intro/
+qed-.
+
+lemma lsubf_inv_bind_sn: ∀g1,f2,I,K1,K2. ⦃K1.ⓘ{I}, ⫯g1⦄ ⫃𝐅* ⦃K2.ⓘ{I}, f2⦄ →
+ ∃∃g2. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f2 = ⫯g2.
+#g1 #f2 * #I [2: #X ] #K1 #K2 #H
+[ elim (lsubf_inv_pair1 … H) -H *
+ [ #z2 #Y2 #H2 #H #H0 destruct /2 width=3 by ex2_intro/
+ | #z #z0 #z2 #Y2 #W #V #_ #_ #_ #_ #H0 #_ #H destruct
+ | #z #z0 #z2 #Z2 #Y2 #_ #_ #_ #_ #H destruct
+ ]
+| elim (lsubf_inv_unit1 … H) -H
+ #z2 #Y2 #H2 #H #H0 destruct /2 width=3 by ex2_intro/
+]
+qed-.
+
+lemma lsubf_inv_beta_sn: ∀g1,f2,K1,K2,V,W. ⦃K1.ⓓⓝW.V, ⫯g1⦄ ⫃𝐅* ⦃K2.ⓛW, f2⦄ →
+ ∃∃g,g0,g2. ⦃K1, g0⦄ ⫃𝐅* ⦃K2, g2⦄ & K1 ⊢ 𝐅*⦃V⦄ ≡ g & g0 ⋓ g ≡ g1 & f2 = ⫯g2.
+#g1 #f2 #K1 #K2 #V #W #H elim (lsubf_inv_pair1 … H) -H *
+[ #z2 #Y2 #_ #_ #H destruct
+| #z #z0 #z2 #Y2 #X0 #X #H02 #Hz #Hg1 #H #_ #H0 #H1 destruct
+ /2 width=7 by ex4_3_intro/
+| #z #z0 #z2 #Z2 #Y2 #_ #_ #_ #_ #H destruct
+]
+qed-.
+
+lemma lsubf_inv_unit_sn: ∀g1,f2,I,J,K1,K2,V. ⦃K1.ⓑ{I}V, ⫯g1⦄ ⫃𝐅* ⦃K2.ⓤ{J}, f2⦄ →
+ ∃∃g,g0,g2. ⦃K1, g0⦄ ⫃𝐅* ⦃K2, g2⦄ & K1 ⊢ 𝐅*⦃V⦄ ≡ g & g0 ⋓ g ≡ g1 & f2 = ⫯g2.
+#g1 #f2 #I #J #K1 #K2 #V #H elim (lsubf_inv_pair1 … H) -H *
+[ #z2 #Y2 #_ #_ #H destruct
+| #z #z0 #z2 #Y2 #X0 #X #_ #_ #_ #_ #_ #_ #H destruct
+| #z #z0 #z2 #Z2 #Y2 #H02 #Hz #Hg1 #H0 #H1 destruct
+ /2 width=7 by ex4_3_intro/
+]
+qed-.
+
+lemma lsubf_inv_refl: ∀L,f1,f2. ⦃L,f1⦄ ⫃𝐅* ⦃L,f2⦄ → f1 ≗ f2.
+#L elim L -L /2 width=1 by lsubf_inv_atom/
+#L #I #IH #f1 #f2 #H12
+elim (pn_split f1) * #g1 #H destruct
+[ elim (lsubf_inv_push_sn … H12) | elim (lsubf_inv_bind_sn … H12) ] -H12
+#g2 #H12 #H destruct /3 width=5 by eq_next, eq_push/
+qed-.
+