| intros; whd; split; assumption
| intros; apply transitive_subseteq_operator; [2: apply f; | skip | assumption]
| intros; cases f; exists [apply w] assumption
- | intros; intros 2; apply (f ? f1 i);
- | intros; intros 2; apply f;
- (* senza questa change, universe inconsistency *)
- whd; change in ⊢ (? ? (λ_:%.?)) with (carr I);
- exists; [apply i] assumption;
+ | intros; split; [ intros 4; apply (f ? f1 i); | intros 3; intro; apply (f i ? f1); ]
+ | intros; split;
+ [ intros 4; apply f; exists; [apply i] assumption;
+ | intros 3; intros; cases f1; apply (f w a x); ]
| intros 3; cases f;
| intros 3; constructor 1;
| intros; cases f; exists; [apply w]
[ assumption
| whd; intros; cases i; simplify; assumption]
| intros; split; intro;
- [ cases f; cases x1;
- (* senza questa change, universe inconsistency *)
- change in ⊢ (? ? (λ_:%.?)) with (carr I);
- exists [apply w1] exists [apply w] assumption;
- | cases e; cases x; exists; [apply w1]
- [ assumption
- | (* senza questa change, universe inconsistency *)
- whd; change in ⊢ (? ? (λ_:%.?)) with (carr I);
- exists; [apply w] assumption]]
+ [ cases f; cases x1; exists [apply w1] exists [apply w] assumption;
+ | cases e; cases x; exists; [apply w1] [ assumption | exists; [apply w] assumption]]
| intros; intros 2; cases (f (singleton ? a) ?);
[ exists; [apply a] [assumption | change with (a = a); apply refl1;]
| change in x1 with (a = w); change with (mem A a q); apply (. (x1‡#));
| change with (a1 ∈ a → ∀x. x ♮(id1 REL o1) a1→x∈a); intros;
change in f1 with (x = a1); apply (. f1‡#); apply f;
| alias symbol "and" = "and_morphism".
- change with ((∃y: carr o1.a1 ♮(id1 REL o1) y ∧ y∈a) → a1 ∈ a);
+ change with ((∃y:o1.a1 ♮(id1 REL o1) y ∧ y∈a) → a1 ∈ a);
intro; cases e; clear e; cases x; clear x; change in f with (a1=w);
apply (. f‡#); apply f1;
- | change with (a1 ∈ a → ∃y: carr o1.a1 ♮(id1 REL o1) y ∧ y∈a);
+ | change with (a1 ∈ a → ∃y:o1.a1 ♮(id1 REL o1) y ∧ y∈a);
intro; exists; [apply a1]; split; [ change with (a1=a1); apply refl1; | apply f]
- | change with ((∃x: carr o1.x ♮(id1 REL o1) a1∧x∈a) → a1 ∈ a);
+ | change with ((∃x:o1.x ♮(id1 REL o1) a1∧x∈a) → a1 ∈ a);
intro; cases e; clear e; cases x; clear x; change in f with (w=a1);
apply (. f^-1‡#); apply f1;
- | change with (a1 ∈ a → ∃x: carr o1.x ♮(id1 REL o1) a1∧x∈a);
+ | change with (a1 ∈ a → ∃x:o1.x ♮(id1 REL o1) a1∧x∈a);
intro; exists; [apply a1]; split; [ change with (a1=a1); apply refl1; | apply f]
| change with ((∀y.a1 ♮(id1 REL o1) y→y∈a) → a1 ∈ a); intros;
apply (f a1); change with (a1 = a1); apply refl1;