matita/matita/contribs/lambdadelta/static_2/etc/frees_drops.etc

   1 lemma frees_sort_pushs:
   2       ∀f,K,s. K ⊢ 𝐅+⦃⋆s⦄ ≘ f →
   3       ∀i,L. ⇩*[i] L ≘ K → L ⊢ 𝐅+⦃⋆s⦄ ≘ ⫯*[i] f.
   4 #f #K #s #Hf #i elim i -i
   5 [ #L #H lapply (drops_fwd_isid … H ?) -H //
   6 | #i #IH #L #H elim (drops_inv_succ … H) -H /3 width=1 by frees_sort/
   7 ]
   8 qed.
   9
  10 lemma frees_gref_pushs:
  11       ∀f,K,l. K ⊢ 𝐅+⦃§l⦄ ≘ f →
  12       ∀i,L. ⇩*[i] L ≘ K → L ⊢ 𝐅+⦃§l⦄ ≘ ⫯*[i] f.
  13 #f #K #l #Hf #i elim i -i
  14 [ #L #H lapply (drops_fwd_isid … H ?) -H //
  15 | #i #IH #L #H elim (drops_inv_succ … H) -H /3 width=1 by frees_gref/
  16 ]
  17 qed.