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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cnf_cif.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cnf_cif.ma
index 51ce95aa0..8ee507cc1 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cnf_cif.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cnf_cif.ma
@@ -96,7 +96,7 @@ lemma cnf_crf_false: ∀L,T. L ⊢ 𝐑⦃T⦄ → L ⊢ 𝐍⦃T⦄ → ⊥.
 | #a #L #V #W #T #H
   elim (cnf_inv_appl … H) -H #_ #_ #H
   elim (simple_inv_bind … H)
-| #a #L #V #W #T #H 
+| #a #L #V #W #T #H
   elim (cnf_inv_appl … H) -H #_ #_ #H
   elim (simple_inv_bind … H)
 ]