(pr3 a x1 x2)
).
Intros until 1; XElim H; Intros.
-(* case 1: pr3_r *)
+(* case 1: pr3_refl *)
XEAuto.
-(* case 1: pr3_r *)
+(* case 1: pr3_refl *)
Pr2GenContext.
LApply (H1 e u d); [ Clear H1; Intros H1 | XAuto ].
LApply (H1 a0); [ Clear H1; Intros H1 | XAuto ].