(x1:?) (subst1 d u t1 (lift (1) d x1)) ->
(x2:?) (subst1 d u t2 (lift (1) d x2)) ->
(pc3 a x1 x2).
- Intros; Pc3Confluence; Repeat Pr3GenContext.
- Subst1Confluence; Rewrite H in H3; Clear H x3; XEAuto.
+ Intros; Pc3Unfold; Repeat Pr3GenContext.
+ Subst1Confluence; Rewrite H3 in H5; Clear H3 x3; XEAuto.
Qed.
End pc3_gen_context.