X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fmodels%2Fq_rebase.ma;h=b14f0bd17bd07fd4a115e38c28257f0890c554fc;hb=HEAD;hp=c521e6bbd7824eb4452d453add96d2d63c102973;hpb=ffa63313d7329be5e1a7b0f40cd31e7102ee0417;p=helm.git

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 c521e6bbd..b14f0bd17 100644
--- a/helm/software/matita/contribs/dama/dama/models/q_rebase.ma
+++ b/helm/software/matita/contribs/dama/dama/models/q_rebase.ma
@@ -12,9 +12,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "russell_support.ma".
+include "dama/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.