[ napply (. Ha^-1) | napply (. Hb^-1) | napply (. Ha) | napply (. Hb)] //.
nqed.
-unification hint 0 ≔ A,B ⊢
- mk_unary_morphism1 …
- (λX.mk_unary_morphism1 … (And X) (prop11 … (and_morphism X)))
- (prop11 … and_morphism)
- A B ≡ And A B.
+unification hint 0 ≔ A,B:CProp[0];
+ T ≟ CPROP,
+ MM ≟ mk_unary_morphism1 ??
+ (λX.mk_unary_morphism1 ?? (And X) (prop11 ?? (fun11 ?? and_morphism X)))
+ (prop11 ?? and_morphism)
+(*-------------------------------------------------------------*) ⊢
+ fun11 T T (fun11 T (unary_morphism1_setoid1 T T) MM A) B ≡ And A B.
(*
naxiom daemon: False.
[ @1; napply (. Ha^-1) | @2; napply (. Hb^-1) | @1; napply (. Ha) | @2; napply (. Hb)] //.
nqed.
-unification hint 0 ≔ A,B ⊢
- mk_unary_morphism1 …
- (λX.mk_unary_morphism1 … (Or X) (prop11 … (or_morphism X)))
- (prop11 … or_morphism)
- A B ≡ Or A B.
-
+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
//.
nqed.
-unification hint 0 ≔ A,B ⊢
- mk_unary_morphism1 …
- (λX:CProp[0].mk_unary_morphism1 … (λY:CProp[0]. X → Y) (prop11 … (if_morphism X)))
- (prop11 … if_morphism)
- A B ≡ A → B.
-
+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.
#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[0];
+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[0].Ex S P)
- (prop11 ?? (Ex_morphism S))
+ 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 S (fun11 (setoid1_of_setoid S) CPROP P).
+ 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[0];
+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[0].Ex S (λx.P x))
- (prop11 ?? (Ex_morphism_eta S))
+ 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 S (λx.fun11 (setoid1_of_setoid S) CPROP P x).
+ fun11 A B M P ≡ Ex (carr S) (λx.fun11 (setoid1_of_setoid S) CPROP P x).
nlemma Ex_setoid : ∀S:setoid.((setoid1_of_setoid S) ⇒_1 CPROP) → setoid.
#T P; @ (Ex T (λx:T.P x)); @; ##[ #H1 H2; napply True |##*: //; ##] nqed.
-unification hint 0 ≔ T,P ;
+unification hint 0 ≔ T : setoid,P ;
S ≟ (Ex_setoid T P)
(*---------------------------*) ⊢
- Ex T (λx:T.P x) ≡ carr S.
+ Ex (carr T) (λx:carr T.fun11 ?? P x) ≡ carr S.
(* couts how many Ex we are traversing *)
ninductive counter : Type[0] ≝