X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Freducibility%2Fcif.ma;h=0a536a914c9e3677244650481ed792b3f9b6cc05;hb=08cb57944c0df08611d4f35d286e46c0d13e4813;hp=0ea9d519b71911f801e2daf417e6a850851e92cd;hpb=9245402674a791dfdb943902f8288d742088c854;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cif.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cif.ma
index 0ea9d519b..0a536a914 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cif.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cif.ma
@@ -38,7 +38,7 @@ lemma cif_inv_bind: ∀a,I,L,V,T. L ⊢ 𝐈⦃ⓑ{a,I}V.T⦄ →
 #a * [ elim a -a ]
 [ #L #V #T #H elim (H ?) -H /3 width=1/
 |*: #L #V #T #H elim (cif_inv_ib2 … H) -H /2 width=1/ /3 width=1/
-]  
+]
 qed-.
 
 lemma cif_inv_appl: ∀L,V,T. L ⊢ 𝐈⦃ⓐV.T⦄ → ∧∧ L ⊢ 𝐈⦃V⦄ & L ⊢ 𝐈⦃T⦄ & 𝐒⦃T⦄.