- MM ≟ mk_unary_morphism1 …
- (λX.mk_unary_morphism1 … (And X) (prop11 … (and_morphism X)))
- (prop11 … and_morphism)
+ 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.
(*-------------------------------------------------------------*) ⊢
fun11 T T (fun11 T (unary_morphism1_setoid1 T T) MM A) B ≡ And A B.
unification hint 0 ≔ A,B:CProp[0];
T ≟ CPROP,
MM ≟ mk_unary_morphism1 …
unification hint 0 ≔ A,B:CProp[0];
T ≟ CPROP,
MM ≟ mk_unary_morphism1 …
(prop11 … or_morphism)
(*-------------------------------------------------------------*) ⊢
fun11 T T (fun11 T (unary_morphism1_setoid1 T T) MM A) B ≡ Or A B.
(prop11 … or_morphism)
(*-------------------------------------------------------------*) ⊢
fun11 T T (fun11 T (unary_morphism1_setoid1 T T) MM A) B ≡ Or A B.
#S; @(λP: (setoid1_of_setoid S) ⇒_1 CProp[0].Ex S P);
#P Q E; @; *; #x Px; @x; ncases (E x x #); /2/; 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.
- 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))
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.
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.
- 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))
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.
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.