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=90ee1e85245752414b93826aabe388409571187a;hp=5ccb5e4accdf9482813b9fe5c8ecb203c46608b9;hpb=e8998d29ab83e7b6aa495a079193705b2f6743d3;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.