include "hints_declaration.ma".
alias symbol "hint_decl" = "hint_decl_Type2".
-unification hint 0 ≔ A ⊢ carr1 (powerclass_setoid A) ≡ Ω^A.
+unification hint 0 ≔ A ⊢ carr1 (mk_setoid1 (Ω^A) (eq1 (powerclass_setoid A))) ≡ Ω^A.
(************ SETS OVER SETOIDS ********************)
unification hint 0 ≔ A ⊢
carr1 (qpowerclass_setoid A) ≡ qpowerclass A.
+(*CSC: non va!
+unification hint 0 ≔ A ⊢
+ carr1 (mk_setoid1 (qpowerclass A) (eq1 (qpowerclass_setoid A))) ≡ qpowerclass A.*)
+
nlemma mem_ok: ∀A. binary_morphism1 (setoid1_of_setoid A) (qpowerclass_setoid A) CPROP.
#A; @
[ napply (λx,S. x ∈ S)
##]
nqed.
+(*CSC: bug qui se metto x o S al posto di ?
+nlemma foo: True.
+nletin xxx ≝ (λA:setoid.λx,S. let SS ≝ pc ? S in
+ fun21 ??? (mk_binary_morphism1 ??? (λx.λS. ? ∈ ?) (prop21 ??? (mem_ok A))) x S);
+*)
unification hint 0 ≔ A:setoid, x, S;
SS ≟ (pc ? S)
(*-------------------------------------*) ⊢
- fun21 ??? (mem_ok A) x S ≡ mem A SS x.
+ fun21 ??? (mk_binary_morphism1 ??? (λx,S. x ∈ S) (prop21 ??? (mem_ok A))) x S ≡ mem A SS x.
nlemma subseteq_ok: ∀A. binary_morphism1 (qpowerclass_setoid A) (qpowerclass_setoid A) CPROP.
#A; @