X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fgrammar%2Fterm.ma;h=9e6e55ed00d70cf598d1a827fb14ef0a0847040e;hb=08cb57944c0df08611d4f35d286e46c0d13e4813;hp=5ccb5e4accdf9482813b9fe5c8ecb203c46608b9;hpb=9245402674a791dfdb943902f8288d742088c854;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/term.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/term.ma
index 5ccb5e4ac..9e6e55ed0 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/term.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/term.ma
@@ -104,7 +104,7 @@ lemma eq_false_inv_tpair_sn: ∀I,V1,T1,V2,T2.
                              (V1 = V2 → ⊥) ∨ (V1 = V2 ∧ (T1 = T2 → ⊥)).
 #I #V1 #T1 #V2 #T2 #H
 elim (term_eq_dec V1 V2) /3 width=1/ #HV12 destruct
-@or_intror @conj // #HT12 destruct /2 width=1/ 
+@or_intror @conj // #HT12 destruct /2 width=1/
 qed-.
 
 lemma eq_false_inv_tpair_dx: ∀I,V1,T1,V2,T2.