unfold minus_star_image in Hletin; unfold singleton in Hletin; simplify in Hletin;
whd in Hletin; whd in Hletin:(?→?→%); simplify in Hletin;
apply (if ?? (A_is_saturation ???));
intros 2 (x H); lapply (Hletin V ? x ?);
unfold minus_star_image in Hletin; unfold singleton in Hletin; simplify in Hletin;
whd in Hletin; whd in Hletin:(?→?→%); simplify in Hletin;
apply (if ?? (A_is_saturation ???));
intros 2 (x H); lapply (Hletin V ? x ?);