...

[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 2186890f0cf29b007e36fd04eb82380637633e49..f75bed7bebe48b7f736ffe18f5324439493dace8 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/models/q_bars.ma
+++ b/helm/software/matita/contribs/dama/dama/models/q_bars.ma
@@ -257,15 +257,14 @@ cases H3; simplify; clear H3; cases H4; clear H4;
   |3: apply (H H3);]
 |4: cases H7; clear H7; cases w in H3 H4 H5 H6 H8; simplify; intros;
     constructor 1; assumption;]
-qed.   
+qed.
 
 definition same_values ≝
   λl1,l2:q_f.
    ∀input.\snd (\fst (value l1 input)) = \snd (\fst (value l2 input)). 
 
 definition same_bases ≝ 
-  λl1,l2:q_f.
-    (∀i.\fst (nth (bars l1) ▭ i) = \fst (nth (bars l2) ▭ i)).
+  λl1,l2:list bar. (∀i.\fst (nth l1 ▭ i) = \fst (nth l2 ▭ i)).
 
 alias symbol "lt" = "Q less than".
 lemma unpos: ∀x:ℚ.OQ < x → ∃r:ratio.Qpos r = x.