-lemma drop_split: ∀L1,L2,l,m2,s. ⬇[s, l, m2] L1 ≡ L2 → ∀m1. m1 ≤ m2 →
- ∃∃L. ⬇[s, l, m2 - m1] L1 ≡ L & ⬇[s, l, m1] L ≡ L2.
-#L1 #L2 #l #m2 #s #H elim H -L1 -L2 -l -m2
-[ #l #m2 #Hs #m1 #Hm12 @(ex2_intro … (⋆))
- @drop_atom #H lapply (Hs H) -s #H destruct /2 width=1 by le_n_O_to_eq/
-| #I #L1 #V #m1 #Hm1 lapply (le_n_O_to_eq … Hm1) -Hm1
- #H destruct /2 width=3 by ex2_intro/
-| #I #L1 #L2 #V #m2 #HL12 #IHL12 #m1 @(nat_ind_plus … m1) -m1
- [ /3 width=3 by drop_drop, ex2_intro/
- | -HL12 #m1 #_ #Hm12 lapply (le_plus_to_le_r … Hm12) -Hm12
- #Hm12 elim (IHL12 … Hm12) -IHL12 >minus_plus_plus_l
- #L #HL1 #HL2 elim (lt_or_ge (|L1|) (m2-m1)) #H0
- [ elim (drop_inv_O1_gt … HL1 H0) -HL1 #H1 #H2 destruct
- elim (drop_inv_atom1 … HL2) -HL2 #H #_ destruct
- @(ex2_intro … (⋆)) [ @drop_O1_ge normalize // ]
- @drop_atom #H destruct
- | elim (drop_O1_pair … HL1 H0 I V) -HL1 -H0 /3 width=5 by drop_drop, ex2_intro/
- ]
- ]
-| #I #L1 #L2 #V1 #V2 #l #m2 #_ #HV21 #IHL12 #m1 #Hm12 elim (IHL12 … Hm12) -IHL12
- #L #HL1 #HL2 elim (lift_split … HV21 l m1) -HV21 /3 width=5 by drop_skip, ex2_intro/
-]
-qed-.
-
lemma drop_inv_refl: ∀L,l,m. ⬇[Ⓕ, l, m] L ≡ L → m = 0.
/2 width=5 by drop_inv_length_eq/ qed-.