+ [ constructor 1;
+ [ apply (λU.image ?? t U);
+ | intros; apply (#‡e); ]
+ | constructor 1;
+ [ apply (λU.minus_star_image ?? t U);
+ | intros; apply (#‡e); ]
+ | constructor 1;
+ [ apply (λU.star_image ?? t U);
+ | intros; apply (#‡e); ]
+ | constructor 1;
+ [ apply (λU.minus_image ?? t U);
+ | intros; apply (#‡e); ]
+ | intros; split; intro;
+ [ change in f with (∀a. a ∈ image ?? t p → a ∈ q);
+ change with (∀a:o1. a ∈ p → a ∈ star_image ?? t q);
+ intros 4; apply f; exists; [apply a] split; assumption;
+ | change in f with (∀a:o1. a ∈ p → a ∈ star_image ?? t q);
+ change with (∀a. a ∈ image ?? t 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 ?? t p → a ∈ q);
+ change with (∀a:o2. a ∈ p → a ∈ minus_star_image ?? t q);
+ intros 4; apply f; exists; [apply a] split; assumption;
+ | change in f with (∀a:o2. a ∈ p → a ∈ minus_star_image ?? t q);
+ change with (∀a. a ∈ minus_image ?? t p → a ∈ q);
+ intros; cases f1; cases x; clear f1 x; apply (f ? f3); assumption; ]
+ | intros; split; intro; cases f; clear f;
+ [ cases x; cases x2; clear x x2; exists; [apply w1]
+ [ assumption;
+ | exists; [apply w] split; assumption]
+ | cases x1; cases x2; clear x1 x2; exists; [apply w1]
+ [ exists; [apply w] split; assumption;
+ | assumption; ]]]
+qed. sistemare anche l'hint da un'altra parte e capire l'exT (doppio!)
\ No newline at end of file