after a PITA, lebergue is dualized!

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

diff --git a/helm/software/matita/contribs/dama/dama/models/q_rebase.ma b/helm/software/matita/contribs/dama/dama/models/q_rebase.ma
index c521e6bbd7824eb4452d453add96d2d63c102973..f8243d6d1979e68c4b0107d8879a003eb36aadab 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/models/q_rebase.ma
+++ b/helm/software/matita/contribs/dama/dama/models/q_rebase.ma
@@ -14,7 +14,7 @@
 
 include "russell_support.ma".
 include "models/q_copy.ma".
-
+(*
 definition rebase_spec ≝ 
  λl1,l2:q_f.λp:q_f × q_f. 
    And3
@@ -88,9 +88,13 @@ intros 6; cases H; simplify; intros; clear H;
   whd; rewrite < H6; apply (inversion_sorted2 ??? H5);
 | apply (sorted_one q2_lt);]
 qed.
+*)
+
+
 
 definition rebase_spec_aux ≝ 
- λl1,l2:list bar.λp:(list bar) × (list bar).
+ λl1,l2
+ :list bar.λp:(list bar) × (list bar).
  sorted q2_lt l1 → (\snd (\last ▭ l1) = 〈OQ,OQ〉) →
  sorted q2_lt l2 → (\snd (\last ▭ l2) = 〈OQ,OQ〉) → 
    rebase_spec_aux_p l1 l2 p.