From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 30 Sep 2009 20:28:17 +0000 (+0000)
Subject: With this hint, it diverges.
X-Git-Tag: make_still_working~3408
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=378f76d39029c959c67cb1761563156ec68d9002;p=helm.git

With this hint, it diverges.
---

diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma
index c32d19436..b09c206ab 100644
--- a/helm/software/matita/nlibrary/sets/sets.ma
+++ b/helm/software/matita/nlibrary/sets/sets.ma
@@ -165,6 +165,13 @@ unification hint 1 ≔
     pc A (mk_qpowerclass ? (B ∩ C) (mem_ok' ? (intersect_ok ? B C))) 
     ≡ intersect ? (pc ? B) (pc ? C).
 
+unification hint 1 ≔ 
+  A : setoid, B,C : qpowerclass A;
+  DX ≟ (intersect ? (pc ? B) (pc ? C)),
+  SX ≟ (mk_qpowerclass ? (B ∩ C) (mem_ok' ? (intersect_ok ? B C)))
+ (*-----------------------------------------------------------------*) ⊢
+  pc A SX  ≡ DX.
+
 nlemma intersect_ok': ∀A. binary_morphism1 (powerclass_setoid A) (powerclass_setoid A) (powerclass_setoid A).
  #A; @ (λS,S'. S ∩ S');
  #a; #a'; #b; #b'; *; #Ha1; #Ha2; *; #Hb1; #Hb2; @; #x; nnormalize; *; #Ka; #Kb; @