With this hint, it diverges.

diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma
index c32d194363d282e57148a028257b1a215f230ba6..b09c206ab774370c2a232f347c84425aecb717b4 100644 (file)
--- 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; @