X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fmodels%2Fq_shift.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fmodels%2Fq_shift.ma;h=a630666595aaee63616e187c98b7bedb54917980;hb=e0b4028cb1f8423b40d5f9ad396f10f42db86f0e;hp=f247fb11d8a9c74b6b8b436da031563e258a2023;hpb=55c78a59b2127ecead99bb814a3ca519f8087053;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.        
+