From: Claudio Sacerdoti Coen 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; @