some more work to factorize out uninteresting parts of the proof...

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

diff --git a/helm/software/matita/contribs/dama/dama/models/q_bars.ma b/helm/software/matita/contribs/dama/dama/models/q_bars.ma
index d0d043f47e053ae50df4e8aaba1ac9f510a83d72..efa45f7f3d3467ab88312f76bed0c9280a1c42ed 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/models/q_bars.ma
+++ b/helm/software/matita/contribs/dama/dama/models/q_bars.ma
@@ -137,11 +137,11 @@ intro; elim l; simplify; intros;
 qed.
 
 lemma sum_bases_O:
-  ∀l:q_f.∀x.sum_bases (bars l) x ≤ OQ → x = O.
+  ∀l.∀x.sum_bases l x ≤ OQ → x = O.
 intros; cases x in H; [intros; reflexivity] intro; cases (?:False);
 cases (q_le_cases ?? H); 
 [1: apply (q_lt_corefl OQ); rewrite < H1 in ⊢ (?? %); 
-|2: apply (q_lt_antisym ??? H1);] clear H H1; cases (bars l);
+|2: apply (q_lt_antisym ??? H1);] clear H H1; cases l;
 simplify; apply q_lt_plus_trans;
 try apply q_pos_lt_OQ; 
 try apply (sum_bases_ge_OQ []);