- Remark pr0_cong_gamma_delta: ~ Abbr = Abst ->
- (u5,t2,w:?) (subst0 (0) u5 t2 w) ->
- (u2,v2,x:?) (pr0 u2 x) -> (pr0 v2 x) ->
- (t5,x0:?) (pr0 t2 x0) -> (pr0 t5 x0) ->
- (u3,x1:?) (pr0 u5 x1) -> (pr0 u3 x1) ->
- (EX t:T | (pr0 (TTail (Flat Appl) u2 (TTail (Bind Abbr) u5 w)) t) &
- (pr0 (TTail (Bind Abbr) u3 (TTail (Flat Appl) (lift (1) (0) v2) t5)) t)).
+ Remark pr0_cong_upsilon_delta: ~ Abbr = Abst ->
+ (u5,t2,w:?) (subst0 (0) u5 t2 w) ->
+ (u2,v2,x:?) (pr0 u2 x) -> (pr0 v2 x) ->
+ (t5,x0:?) (pr0 t2 x0) -> (pr0 t5 x0) ->
+ (u3,x1:?) (pr0 u5 x1) -> (pr0 u3 x1) ->
+ (EX t:T | (pr0 (TTail (Flat Appl) u2 (TTail (Bind Abbr) u5 w)) t) &
+ (pr0 (TTail (Bind Abbr) u3 (TTail (Flat Appl) (lift (1) (0) v2) t5)) t)).