...

[helm.git] / helm / software / matita / contribs / dama / dama / models / q_shift.ma

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 f247fb11d8a9c74b6b8b436da031563e258a2023..a630666595aaee63616e187c98b7bedb54917980 100644 (file)
--- 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.        
+