- improved Makefile esp. with the "trim" function

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cif.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cif.ma
index 0ea9d519b71911f801e2daf417e6a850851e92cd..0a536a914c9e3677244650481ed792b3f9b6cc05 100644 (file)
--- 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⦄.