+nlemma test: ∀A,A',B: CProp[0]. A=A' → (B ∨ A) = B → (B ∧ A) ∧ B.
+ #A; #A'; #B; #H1; #H2; napply (. (#‡H1)‡H2^-1); nelim daemon.
+nqed.
+
+CSC: ugly proof term
+ncheck test.
+*)
+
+ndefinition or_morphism: unary_morphism1 CPROP (unary_morphism1_setoid1 CPROP CPROP).
+ napply (mk_binary_morphism1 … Or);
+ #a; #a'; #b; #b'; #Ha; #Hb; @; *; #x
+ [ @1; napply (. Ha^-1) | @2; napply (. Hb^-1) | @1; napply (. Ha) | @2; napply (. Hb)] //.
+nqed.
+
+unification hint 0 ≔ A,B:CProp[0];
+ T ≟ CPROP,
+ MM ≟ mk_unary_morphism1 …
+ (λX.mk_unary_morphism1 … (Or X) (prop11 … (fun11 ?? or_morphism X)))
+ (prop11 … or_morphism)
+(*-------------------------------------------------------------*) ⊢
+ fun11 T T (fun11 T (unary_morphism1_setoid1 T T) MM A) B ≡ Or A B.
+
+(* XXX always applied, generates hard unif problems
+ndefinition if_morphism: unary_morphism1 CPROP (unary_morphism1_setoid1 CPROP CPROP).
+ napply (mk_binary_morphism1 … (λA,B:CProp[0]. A → B));
+ #a; #a'; #b; #b'; #Ha; #Hb; @; #H; #x
+ [ napply (. Hb^-1); napply H; napply (. Ha) | napply (. Hb); napply H; napply (. Ha^-1)]
+ //.
+nqed.
+
+unification hint 0 ≔ A,B:CProp[0];
+ T ≟ CPROP,
+ R ≟ mk_unary_morphism1 …
+ (λX:CProp[0].mk_unary_morphism1 …
+ (λY:CProp[0]. X → Y) (prop11 … (if_morphism X)))
+ (prop11 … if_morphism)
+(*----------------------------------------------------------------------*) ⊢
+ fun11 T T (fun11 T (unary_morphism1_setoid1 T T) R A) B ≡ A → B.
+*)
+
+(* not as morphism *)
+nlemma Not_morphism : CProp[0] ⇒_1 CProp[0].
+@(λx:CProp[0].¬ x); #a b; *; #; @; /3/; nqed.
+
+unification hint 0 ≔ P : CProp[0];
+ A ≟ CPROP,
+ B ≟ CPROP,
+ M ≟ mk_unary_morphism1 ?? (λP.¬ P) (prop11 ?? Not_morphism)
+(*------------------------*)⊢
+ fun11 A B M P ≡ ¬ P.
+
+(* Ex setoid support *)
+
+(* The caml, as some patches for it
+ncoercion setoid1_of_setoid : ∀s:setoid. setoid1 ≝ setoid1_of_setoid on _s: setoid to setoid1.
+*)
+
+(* simple case where the whole predicate can be rewritten *)
+nlemma Ex_morphism : ∀S:setoid.((setoid1_of_setoid S) ⇒_1 CProp[0]) ⇒_1 CProp[0].
+#S; @(λP: (setoid1_of_setoid S) ⇒_1 CProp[0].Ex S P);
+#P Q E; @; *; #x Px; @x; ncases (E x x #); /2/; nqed.
+
+unification hint 0 ≔ S : setoid, P : (setoid1_of_setoid S) ⇒_1 CPROP;
+ A ≟ unary_morphism1_setoid1 (setoid1_of_setoid S) CPROP,
+ B ≟ CPROP,
+ M ≟ mk_unary_morphism1 ??
+ (λP: (setoid1_of_setoid S) ⇒_1 CPROP.Ex (carr S) (fun11 ?? P))
+ (prop11 ?? (Ex_morphism S))
+(*------------------------*)⊢
+ fun11 A B M P ≡ Ex (carr S) (fun11 (setoid1_of_setoid S) CPROP P).
+
+nlemma Ex_morphism_eta : ∀S:setoid.((setoid1_of_setoid S) ⇒_1 CProp[0]) ⇒_1 CProp[0].
+#S; @(λP: (setoid1_of_setoid S) ⇒_1 CProp[0].Ex S (λx.P x));
+#P Q E; @; *; #x Px; @x; ncases (E x x #); /2/; nqed.
+
+unification hint 0 ≔ S : setoid, P : (setoid1_of_setoid S) ⇒_1 CPROP;
+ A ≟ unary_morphism1_setoid1 (setoid1_of_setoid S) CPROP,
+ B ≟ CPROP,
+ M ≟ mk_unary_morphism1 ??
+ (λP: (setoid1_of_setoid S) ⇒_1 CPROP.Ex (carr S) (λx.fun11 ?? P x))
+ (prop11 ?? (Ex_morphism_eta S))
+(*------------------------*)⊢
+ fun11 A B M P ≡ Ex (carr S) (λx.fun11 (setoid1_of_setoid S) CPROP P x).