(* *)
(**************************************************************************)
+include "hints_declaration.ma".
include "sets/setoids1.ma".
ndefinition CPROP: setoid1.
[ napply (H3 (H1 w)) | napply (H2 (H4 w))]##]##]
nqed.
-unification hint 0 ((λx,y.True) (carr1 CPROP) CProp[0]).
+alias symbol "hint_decl" = "hint_decl_CProp2".
+unification hint 0 ≔ ⊢ CProp[0] ≡ carr1 CPROP.
(*ndefinition CProp0_of_CPROP: carr1 CPROP → CProp[0] ≝ λx.x.
ncoercion CProp0_of_CPROP : ∀x: carr1 CPROP. CProp[0] ≝ CProp0_of_CPROP
| napply (H4 K2)]##]
nqed.
-unification hint 0 (∀A,B.(λx,y.True) (fun21 ??? and_morphism A B) (And A B)).
+(*unification hint 0 ≔ A,B ⊢ fun21 … and_morphism A B ≡ And A B.*)
+unification hint 0 ≔ A,B ⊢ fun21 … (mk_binary_morphism1 … And (prop21 … and_morphism)) A B ≡ And A B.
+
+(*nlemma test: ∀A,A',B: CProp[0]. A=A' → (B ∨ A) = B → (B ∧ A) ∧ B.
+ #A; #A'; #B; #H1; #H2;
+ napply (. ((#‡H1)‡H2^-1)); nnormalize;
+nqed.*)
+
(*nlemma test: ∀A,A',B: CProp[0]. A=A' → (B ∨ A) = B → (B ∧ A) ∧ B.
#A; #A'; #B; #H1; #H2;
| napply (H4 H)]##]
nqed.
-unification hint 0 (∀A,B.(λx,y.True) (fun21 ??? or_morphism A B) (Or A B)).
+unification hint 0 ≔ A,B ⊢ fun21 … or_morphism A B ≡ Or A B.
(*interpretation "or_morphism" 'or a b = (fun21 ??? or_morphism a b).*)