first definition of cpm:

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / static / frees_drops.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma
index 441d3c51f5670ff8298c9f8f35738024078f3102..c5762eacbbe202d8c246ec8f26d0bb63782efc5f 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma
@@ -49,7 +49,8 @@ lemma frees_lref_pushs: ∀f,K,j. K ⊢ 𝐅*⦃#j⦄ ≡ f →
                         ∀i,L. ⬇*[i] L ≡ K → L ⊢ 𝐅*⦃#(i+j)⦄ ≡ ↑*[i] f.
 #f #K #j #Hf #i elim i -i
 [ #L #H lapply (drops_fwd_isid … H ?) -H //
-| #i #IH #L #H elim (drops_inv_succ … H) -H /3 width=1 by frees_lref/
+| #i #IH #L #H elim (drops_inv_succ … H) -H
+  #I #Y #V #HYK #H destruct /3 width=1 by frees_lref/
 ]
 qed.