- #A; napply mk_binary_morphism1
- [ napply (λx.λS: qpowerclass_setoid A. x ∈ S) (* CSC: ??? *)
- | #a; #a'; #b; #b'; #Ha; #Hb; (* CSC: qui *; non funziona *)
- nwhd; nwhd in ⊢ (? (? % ??) (? % ??)); napply mk_iff; #H
- [ ncases Hb; #Hb1; #_; napply Hb1; napply (. (mem_ok' …))
- [ nassumption | napply Ha^-1 | ##skip ]
- ##| ncases Hb; #_; #Hb2; napply Hb2; napply (. (mem_ok' …))
- [ nassumption | napply Ha | ##skip ]##]
-nqed.
-
-unification hint 0 (∀A,x,S. (λx,y.True) (fun21 ??? (mem_ok A) x S) (mem A S x)).
-
+ #A; @
+ [ napply (λx,S. x ∈ S)
+ | #a; #a'; #b; #b'; #Ha; *; #Hb1; #Hb2; @; #H;
+ ##[ napply Hb1; napply (. (mem_ok' …)); ##[##3: napply H| napply Ha^-1;##]
+ ##| napply Hb2; napply (. (mem_ok' …)); ##[##3: napply H| napply Ha;##]
+ ##]
+ ##]
+nqed.
+
+unification hint 0 ≔ A:setoid, x, S;
+ SS ≟ (pc ? S)
+ (*-------------------------------------*) ⊢
+ fun21 ??? (mem_ok A) x S ≡ mem A SS x.
+