-theorem lfxs_conf: ∀R. lexs_frees_confluent R cfull →
- R_confluent2_lfxs R R R R →
- ∀T. confluent … (lfxs R T).
-#R #H1R #H2R #T #L0 #L1 * #f1 #Hf1 #HL01 #L2 * #f #Hf #HL02
-lapply (frees_mono … Hf1 … Hf) -Hf1 #Hf12
-lapply (lexs_eq_repl_back … HL01 … Hf12) -f1 #HL01
-elim (lexs_conf … HL01 … HL02) /2 width=3 by ex2_intro/ [ | -HL01 -HL02 ]
-[ #L #HL1 #HL2
- elim (H1R … Hf … HL01) -HL01 #f1 #Hf1 #H1
- elim (H1R … Hf … HL02) -HL02 #f2 #Hf2 #H2
- lapply (sle_lexs_trans … HL1 … H1) // -HL1 -H1 #HL1
- lapply (sle_lexs_trans … HL2 … H2) // -HL2 -H2 #HL2
- /3 width=5 by ex2_intro/
-| #g #I #K0 #V0 #n #HLK0 #Hgf #V1 #HV01 #V2 #HV02 #K1 #HK01 #K2 #HK02
- elim (frees_drops_next … Hf … HLK0 … Hgf) -Hf -HLK0 -Hgf #g0 #Hg0 #H0
- lapply (sle_lexs_trans … HK01 … H0) // -HK01 #HK01
- lapply (sle_lexs_trans … HK02 … H0) // -HK02 #HK02
- elim (H2R … HV01 … HV02 K1 … K2) /2 width=3 by ex2_intro/
-]
+theorem lfxs_bind_void: ∀R,p,I,L1,L2,V,T.
+ L1 ⪤*[R, V] L2 → L1.ⓧ ⪤*[R, T] L2.ⓧ →
+ L1 ⪤*[R, ⓑ{p,I}V.T] L2.
+#R #p #I #L1 #L2 #V #T * #f1 #HV #Hf1 * #f2 #HT #Hf2
+lapply (lexs_fwd_bind … Hf2) -Hf2 #Hf2 elim (sor_isfin_ex f1 (⫱f2))
+/3 width=7 by frees_fwd_isfin, frees_bind_void, lexs_join, isfin_tl, ex2_intro/
+qed.
+
+(* Negated inversion lemmas *************************************************)
+
+(* Basic_2A1: uses: nllpx_sn_inv_bind nllpx_sn_inv_bind_O *)
+lemma lfnxs_inv_bind: ∀R. (∀L,T1,T2. Decidable (R L T1 T2)) →
+ ∀p,I,L1,L2,V,T. (L1 ⪤*[R, ⓑ{p,I}V.T] L2 → ⊥) →
+ (L1 ⪤*[R, V] L2 → ⊥) ∨ (L1.ⓑ{I}V ⪤*[R, T] L2.ⓑ{I}V → ⊥).
+#R #HR #p #I #L1 #L2 #V #T #H elim (lfxs_dec … HR L1 L2 V)
+/4 width=2 by lfxs_bind, or_intror, or_introl/
+qed-.
+
+(* Basic_2A1: uses: nllpx_sn_inv_flat *)
+lemma lfnxs_inv_flat: ∀R. (∀L,T1,T2. Decidable (R L T1 T2)) →
+ ∀I,L1,L2,V,T. (L1 ⪤*[R, ⓕ{I}V.T] L2 → ⊥) →
+ (L1 ⪤*[R, V] L2 → ⊥) ∨ (L1 ⪤*[R, T] L2 → ⊥).
+#R #HR #I #L1 #L2 #V #T #H elim (lfxs_dec … HR L1 L2 V)
+/4 width=1 by lfxs_flat, or_intror, or_introl/
+qed-.
+
+lemma lfnxs_inv_bind_void: ∀R. (∀L,T1,T2. Decidable (R L T1 T2)) →
+ ∀p,I,L1,L2,V,T. (L1 ⪤*[R, ⓑ{p,I}V.T] L2 → ⊥) →
+ (L1 ⪤*[R, V] L2 → ⊥) ∨ (L1.ⓧ ⪤*[R, T] L2.ⓧ → ⊥).
+#R #HR #p #I #L1 #L2 #V #T #H elim (lfxs_dec … HR L1 L2 V)
+/4 width=2 by lfxs_bind_void, or_intror, or_introl/