3 Require subst1_confluence.
5 Require pr3_gen_context.
9 Section pc3_gen_context. (************************************************)
11 Theorem pc3_gen_cabbr: (c:?; t1,t2:?) (pc3 c t1 t2) -> (e:?; u:?; d:?)
12 (drop d (0) c (CTail e (Bind Abbr) u)) ->
13 (a0:?) (csubst1 d u c a0) ->
14 (a:?) (drop (1) d a0 a) ->
15 (x1:?) (subst1 d u t1 (lift (1) d x1)) ->
16 (x2:?) (subst1 d u t2 (lift (1) d x2)) ->
18 Intros; Pc3Unfold; Repeat Pr3GenContext.
19 Subst1Confluence; Rewrite H3 in H5; Clear H3 x3; XEAuto.