- Theorem pr2_gen_abbr : (c:?; u1,t1,x:?)
- (pr2 c (TTail (Bind Abbr) u1 t1) x) ->
- (EX u2 t2 | x = (TTail (Bind Abbr) u2 t2) &
- (pr2 c u1 u2) &
- ((b:?; u:?) (pr2 (CTail c (Bind b) u) t1 t2)) \/
- (EX y | (pr0 t1 y) & (subst0 (0) u2 y t2))
- ) \/
- (pr0 t1 (lift (1) (0) x)).
- Intros; Inversion H;
- Try Pr0Gen; Try Subst0Gen; XDEAuto 8.
+ Theorem pr2_gen_abbr: (c:?; u1,t1,x:?)
+ (pr2 c (TTail (Bind Abbr) u1 t1) x) ->
+ (EX u2 t2 | x = (TTail (Bind Abbr) u2 t2) &
+ (pr2 c u1 u2) & (OR
+ (b:?; u:?) (pr2 (CTail c (Bind b) u) t1 t2) |
+ (EX u | (pr0 u1 u) & (pr2 (CTail c (Bind Abbr) u) t1 t2)) |
+ (EX y z | (pr2 (CTail c (Bind Abbr) u1) t1 y) & (pr0 y z) & (pr2 (CTail c (Bind Abbr) u1) z t2))
+ )) \/ (b:?; u:?)
+ (pr2 (CTail c (Bind b) u) t1 (lift (1) (0) x)).
+ Intros; Inversion H;
+ Pr0Gen; Try Rewrite H1 in H2; Try Subst0Gen; Try Pr0Subst0; XDEAuto 10.