-
-(* Inversion lemmas on negated lazy pointwise extension *********************)
-
-lemma nllpx_sn_inv_bind: ∀R. (∀L,T1,T2. Decidable (R L T1 T2)) →
- ∀a,I,L1,L2,V,T,l. (llpx_sn R l (ⓑ{a,I}V.T) L1 L2 → ⊥) →
- (llpx_sn R l V L1 L2 → ⊥) ∨ (llpx_sn R (⫯l) T (L1.ⓑ{I}V) (L2.ⓑ{I}V) → ⊥).
-#R #HR #a #I #L1 #L2 #V #T #l #H elim (llpx_sn_dec … HR V L1 L2 l)
-/4 width=1 by llpx_sn_bind, or_intror, or_introl/
-qed-.
-
-lemma nllpx_sn_inv_flat: ∀R. (∀L,T1,T2. Decidable (R L T1 T2)) →
- ∀I,L1,L2,V,T,l. (llpx_sn R l (ⓕ{I}V.T) L1 L2 → ⊥) →
- (llpx_sn R l V L1 L2 → ⊥) ∨ (llpx_sn R l T L1 L2 → ⊥).
-#R #HR #I #L1 #L2 #V #T #l #H elim (llpx_sn_dec … HR V L1 L2 l)
-/4 width=1 by llpx_sn_flat, or_intror, or_introl/
-qed-.
-
-lemma nllpx_sn_inv_bind_O: ∀R. (∀L,T1,T2. Decidable (R L T1 T2)) →
- ∀a,I,L1,L2,V,T. (llpx_sn R 0 (ⓑ{a,I}V.T) L1 L2 → ⊥) →
- (llpx_sn R 0 V L1 L2 → ⊥) ∨ (llpx_sn R 0 T (L1.ⓑ{I}V) (L2.ⓑ{I}V) → ⊥).
-#R #HR #a #I #L1 #L2 #V #T #H elim (llpx_sn_dec … HR V L1 L2 0)
-/4 width=1 by llpx_sn_bind_O, or_intror, or_introl/
-qed-.