- improved Makefile esp. with the "trim" function

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / reducibility / cnf_cif.ma

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 51ce95aa066356cb2f94e304e38727f00d6aa7b3..8ee507cc14c1fa421326b2982f258bf56d0c79e3 100644 (file)
--- 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)
 ]