- Theorem pr2_gen_appl : (c:?; u1,t1,x:?)
- (pr2 c (TTail (Flat Appl) u1 t1) x) -> (OR
- (EX u2 t2 | x = (TTail (Flat Appl) u2 t2) &
- (pr2 c u1 u2) & (pr2 c t1 t2)
- ) |
- (EX y1 z1 u2 t2 | t1 = (TTail (Bind Abst) y1 z1) &
- x = (TTail (Bind Abbr) u2 t2) &
- (pr0 u1 u2) & (pr0 z1 t2)
- ) |
- (EX b y1 z1 u2 v2 t2 |
- ~b=Abst &
- t1 = (TTail (Bind b) y1 z1) &
- x = (TTail (Bind b) v2 (TTail (Flat Appl) (lift (1) (0) u2) t2)) &
- (pr0 u1 u2) & (pr0 y1 v2) & (pr0 z1 t2))
- ).
- Intros; Inversion H;
- Try Pr0GenBase; Try Subst0GenBase; XEAuto.
+ Theorem pr2_gen_appl: (c:?; u1,t1,x:?)
+ (pr2 c (TTail (Flat Appl) u1 t1) x) -> (OR
+ (EX u2 t2 | x = (TTail (Flat Appl) u2 t2) &
+ (pr2 c u1 u2) & (pr2 c t1 t2)
+ ) |
+ (EX y1 z1 u2 t2 | t1 = (TTail (Bind Abst) y1 z1) &
+ x = (TTail (Bind Abbr) u2 t2) &
+ (pr2 c u1 u2) & (b:?; u:?)
+ (pr2 (CTail c (Bind b) u) z1 t2)
+ ) |
+ (EX b y1 z1 z2 u2 v2 t2 |
+ ~b=Abst &
+ t1 = (TTail (Bind b) y1 z1) &
+ x = (TTail (Bind b) v2 z2) &
+ (pr2 c u1 u2) & (pr2 c y1 v2) & (pr0 z1 t2))
+ ).
+ Intros; Inversion H; Pr0GenBase;
+ Try Rewrite H1 in H2; Try Rewrite H4 in H2; Try Rewrite H5 in H2;
+ Try Subst0GenBase; XDEAuto 7.