interpretation "subset comprehension" 'comprehension s p =
(comprehension s (mk_unary_morphism __ p _)).
-definition ext: ∀X,S:REL. ∀r: arrows1 ? X S. S ⇒ Ω \sup X.
- apply (λX,S,r.mk_unary_morphism ?? (λf.{x ∈ X | x ♮r f}) ?);
+definition ext: ∀X,S:REL. binary_morphism1 (arrows1 ? X S) S (Ω \sup X).
+ apply (λX,S.mk_binary_morphism1 ??? (λr:arrows1 ? X S.λf:S.{x ∈ X | x ♮r f}) ?);
[ intros; simplify; apply (.= (H‡#)); apply refl1
- | intros; simplify; split; intros; simplify; intros;
- [ apply (. #‡(#‡H)); assumption
- | apply (. #‡(#‡H\sup -1)); assumption]]
+ | intros; simplify; split; intros; simplify; intros; cases f; split; try assumption;
+ [ apply (. (#‡H1)); whd in H; apply (if ?? (H ??)); assumption
+ | apply (. (#‡H1\sup -1)); whd in H; apply (fi ?? (H ??));assumption]]
qed.
definition extS: ∀X,S:REL. ∀r: arrows1 ? X S. Ω \sup S ⇒ Ω \sup X.
| change with (a = a); apply refl]]]
qed.
-lemma extS_com: ∀o1,o2,o3,c1,c2,S. extS o1 o3 (c1 ∘ c2) S = extS o1 o2 c1 (extS o2 o3 c2 S).
+lemma extS_com: ∀o1,o2,o3,c1,c2,S. extS o1 o3 (c2 ∘ c1) S = extS o1 o2 c1 (extS o2 o3 c2 S).
intros; unfold extS; simplify; split; intros; simplify; intros;
[ cases f (H1 H2); cases H2 (w H3); clear f H2; split; [assumption]
cases H3 (H4 H5); cases H5 (w1 H6); clear H3 H5; cases H6 (H7 H8); clear H6;