- [ change in f with (∀a. a ∈ image ?? c p → a ∈ q);
- change with (∀a:o1. a ∈ p → a ∈ star_image ?? c q);
- intros 4; apply f; exists; [apply a] split; assumption;
- | change in f with (∀a:o1. a ∈ p → a ∈ star_image ?? c q);
- change with (∀a. a ∈ image ?? c p → a ∈ q);
- intros; cases f1; cases x; clear f1 x; apply (f ? f3); assumption; ]
- | intros; split; intro;
- [ change in f with (∀a. a ∈ minus_image ?? c p → a ∈ q);
- change with (∀a:o2. a ∈ p → a ∈ minus_star_image ?? c q);
- intros 4; apply f; exists; [apply a] split; assumption;
- | change in f with (∀a:o2. a ∈ p → a ∈ minus_star_image ?? c q);
- change with (∀a. a ∈ minus_image ?? c p → a ∈ q);
- intros; cases f1; cases x; clear f1 x; apply (f ? f3); assumption; ]
- | intros; split; intro; cases f; clear f;
+ [ intros 2; intros 2; apply (f y); exists[apply a] split; assumption;
+ | intros 2; change with (a ∈ q); cases f1; cases x; clear f1 x;
+ apply (f w f3); assumption; ]
+ | unfold foo; intros; split; intro;
+ [ intros 2; intros 2; apply (f x); exists [apply a] split; assumption;
+ | intros 2; change with (a ∈ q); cases f1; cases x; apply (f w f3); assumption;]
+ | intros; split; unfold foo; unfold image_coercion; simplify; intro; cases f; clear f;