matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops.etc

   1 lemma drop_inv_refl: ∀L,l,m. ⬇[Ⓕ, l, m] L ≡ L → m = 0.
   2 /2 width=5 by drop_inv_length_eq/ qed-.
   3
   4 fact drop_inv_FT_aux: ∀L1,L2,s,l,m. ⬇[s, l, m] L1 ≡ L2 →
   5                       ∀I,K,V. L2 = K.ⓑ{I}V → s = Ⓣ → l = 0 →
   6                       ⬇[Ⓕ, l, m] L1 ≡ K.ⓑ{I}V.
   7 #L1 #L2 #s #l #m #H elim H -L1 -L2 -l -m
   8 [ #l #m #_ #J #K #W #H destruct
   9 | #I #L #V #J #K #W #H destruct //
  10 | #I #L1 #L2 #V #m #_ #IHL12 #J #K #W #H1 #H2 destruct
  11   /3 width=1 by drop_drop/
  12 | #I #L1 #L2 #V1 #V2 #l #m #_ #_ #_ #J #K #W #_ #_ #H
  13   elim (ysucc_inv_O_dx … H)
  14 ]
  15 qed-.
  16
  17 lemma drop_inv_FT: ∀I,L,K,V,m. ⬇[Ⓣ, 0, m] L ≡ K.ⓑ{I}V → ⬇[m] L ≡
  18 K.ⓑ{I}V.
  19 /2 width=5 by drop_inv_FT_aux/ qed.
  20
  21 lemma drop_inv_gen: ∀I,L,K,V,s,m. ⬇[s, 0, m] L ≡ K.ⓑ{I}V → ⬇[m] L ≡
  22 K.ⓑ{I}V.
  23 #I #L #K #V * /2 width=1 by drop_inv_FT/
  24 qed-.
  25
  26 lemma drop_inv_T: ∀I,L,K,V,s,m. ⬇[Ⓣ, 0, m] L ≡ K.ⓑ{I}V → ⬇[s, 0, m] L
  27 ≡ K.ⓑ{I}V.
  28 #I #L #K #V * /2 width=1 by drop_inv_FT/
  29 qed-.