|2: intros 4 (U H x Hx); simplify in Hx;
cases H (_ H1); cases (H1 x); apply H2; apply Hx;
|3: intros; cases H (_ PU); cases H1 (_ PV);
|2: intros 4 (U H x Hx); simplify in Hx;
cases H (_ H1); cases (H1 x); apply H2; apply Hx;
|3: intros; cases H (_ PU); cases H1 (_ PV);