X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fmodels%2Fq_shift.ma;h=a630666595aaee63616e187c98b7bedb54917980;hb=910c252965fe17d6b5af92e4658e7d02bac82d58;hp=f247fb11d8a9c74b6b8b436da031563e258a2023;hpb=d03c932e859d59c0ae381f941b4003d744b6b106;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama/models/q_shift.ma b/helm/software/matita/contribs/dama/dama/models/q_shift.ma
index f247fb11d..a63066659 100644
--- a/helm/software/matita/contribs/dama/dama/models/q_shift.ma
+++ b/helm/software/matita/contribs/dama/dama/models/q_shift.ma
@@ -103,3 +103,4 @@ cases Hv1 (HV1 HV1 HV1 HV1); cases HV1 (Hi1 Hv11 Hv12); clear HV1 Hv1;
       |1: apply solution; apply (q_eq_to_le ?? (sym_eq ??? H4));
       |3: apply solution; apply (q_lt_to_le ?? H4);]
 qed.        
+