X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fsubstitution%2Fcofrees_lift.ma;h=b8e4542a7973fafbe2a7b7c29750b4fa18dbd096;hb=a0d25627e80a3a2fe68da954b68f6d541c6dbc34;hp=30bcd9ce945f7bb7d9726f1709cc5885b80fae3c;hpb=42da17037d96c9c8e95a21ea71aa70522916939a;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cofrees_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cofrees_lift.ma
index 30bcd9ce9..b8e4542a7 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cofrees_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cofrees_lift.ma
@@ -95,3 +95,11 @@ lemma frees_inv_gen: ∀L,U,d,i. (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥) →
   /4 width=9 by cpys_flat, nlift_flat_dx, nlift_flat_sn, ex2_intro/
 ]
 qed-.
+
+lemma frees_ind: ∀L,d,i. ∀R:predicate term.
+                 (∀U1. (∀T1. ⇧[i, 1] T1 ≡ U1 → ⊥) → R U1) → 
+                 (∀U1,U2. ⦃⋆, L⦄ ⊢ U1 ▶[d, ∞] U2 → (L ⊢ i ~ϵ 𝐅*[d]⦃U2⦄ → ⊥) → R U2 → R U1) →
+                 ∀U. (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥) → R U.
+#L #d #i #R #IH1 #IH2 #U1 #H elim (frees_inv_gen … H) -H
+#U2 #H #HnU2 @(cpys_ind_dx … H) -U1 /4 width=8 by cofrees_inv_gen/
+qed-.