- Remark pr2_pr0_delta: (c,d:?; t0,t1,t2,u:?; i:?)
- (pr0 t0 t1) ->
- (drop i (0) c (CTail d (Bind Abbr) u)) ->
- (subst0 i u t0 t2) ->
- (EX t | (pr2 c t1 t) & (pr2 c t2 t)).
- Intros; Pr0Subst0; XEAuto.
+ Remark pr2_free_delta: (c,d:?; t0,t1,t2,t4,u:?; i:?)
+ (pr0 t0 t1) ->
+ (drop i (0) c (CTail d (Bind Abbr) u)) ->
+ (pr0 t0 t4) ->
+ (subst0 i u t4 t2) ->
+ (EX t | (pr2 c t1 t) & (pr2 c t2 t)).
+ Intros; Pr0Confluence; Pr0Subst0; XEAuto.