+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "sets/setoids1.ma".
+
+ndefinition CPROP: setoid1.
+ napply mk_setoid1
+ [ napply CProp[0]
+ | napply (mk_equivalence_relation1 CProp[0])
+ [ napply iff
+ | #x; napply mk_iff; #H; nassumption
+ | #x; #y; *; #H1; #H2; napply mk_iff; nassumption
+ | #x; #y; #z; *; #H1; #H2; *; #H3; #H4; napply mk_iff; #w
+ [ napply (H3 (H1 w)) | napply (H2 (H4 w))]##]##]
+nqed.
+
+unification hint 0 ((λx,y.True) (carr1 CPROP) CProp[0]).
+
+(*ndefinition CProp0_of_CPROP: carr1 CPROP → CProp[0] ≝ λx.x.
+ncoercion CProp0_of_CPROP : ∀x: carr1 CPROP. CProp[0] ≝ CProp0_of_CPROP
+ on _x: carr1 CPROP to CProp[0].*)
+
+alias symbol "eq" = "setoid1 eq".
+
+ndefinition fi': ∀A,B:CPROP. A = B → B → A.
+ #A; #B; #H; napply (fi … H); nassumption.
+nqed.
+
+notation ". r" with precedence 50 for @{'fi $r}.
+interpretation "fi" 'fi r = (fi' ?? r).
+
+ndefinition and_morphism: binary_morphism1 CPROP CPROP CPROP.
+ napply mk_binary_morphism1
+ [ napply And
+ | #a; #a'; #b; #b'; *; #H1; #H2; *; #H3; #H4; napply mk_iff; *; #K1; #K2; napply conj
+ [ napply (H1 K1)
+ | napply (H3 K2)
+ | napply (H2 K1)
+ | napply (H4 K2)]##]
+nqed.
+
+unification hint 0 (∀A,B.(λx,y.True) (fun21 ??? 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.*)
+
+(*interpretation "and_morphism" 'and a b = (fun21 ??? and_morphism a b).*)
+
+ndefinition or_morphism: binary_morphism1 CPROP CPROP CPROP.
+ napply mk_binary_morphism1
+ [ napply Or
+ | #a; #a'; #b; #b'; *; #H1; #H2; *; #H3; #H4; napply mk_iff; *; #H;
+ ##[##1,3: napply or_introl |##*: napply or_intror ]
+ ##[ napply (H1 H)
+ | napply (H2 H)
+ | napply (H3 H)
+ | napply (H4 H)]##]
+nqed.
+
+unification hint 0 (∀A,B.(λx,y.True) (fun21 ??? or_morphism A B) (Or A B)).
+
+(*interpretation "or_morphism" 'or a b = (fun21 ??? or_morphism a b).*)
+
+ndefinition if_morphism: binary_morphism1 CPROP CPROP CPROP.
+ napply mk_binary_morphism1
+ [ napply (λA,B. A → B)
+ | #a; #a'; #b; #b'; #H1; #H2; napply mk_iff; #H; #w
+ [ napply (if … H2); napply H; napply (fi … H1); nassumption
+ | napply (fi … H2); napply H; napply (if … H1); nassumption]##]
+nqed.
\ No newline at end of file