generalize in match H5; generalize in match H8;
generalize in match (PU x); clear H6 H7 H1 H4 H2 H3 H5 H8;
cases x; simplify; intros; cases H1; clear H1; apply H4;
generalize in match H5; generalize in match H8;
generalize in match (PU x); clear H6 H7 H1 H4 H2 H3 H5 H8;
cases x; simplify; intros; cases H1; clear H1; apply H4;