- | pr0_beta : (k,v1,v2:?) (pr0 v1 v2) -> (t1,t2:?) (pr0 t1 t2) ->
- (pr0 (TTail (Flat Appl) v1 (TTail (Bind Abst) k t1))
- (TTail (Bind Abbr) v2 t2))
- | pr0_gamma : (b:?) ~b=Abst -> (v1,v2:?) (pr0 v1 v2) ->
- (u1,u2:?) (pr0 u1 u2) -> (t1,t2:?) (pr0 t1 t2) ->
- (pr0 (TTail (Flat Appl) v1 (TTail (Bind b) u1 t1))
- (TTail (Bind b) u2 (TTail (Flat Appl) (lift (1) (0) v2) t2)))
- | pr0_delta : (u1,u2:?) (pr0 u1 u2) -> (t1,t2:?) (pr0 t1 t2) ->
- (w:?) (subst0 (0) u2 t2 w) ->
- (pr0 (TTail (Bind Abbr) u1 t1) (TTail (Bind Abbr) u2 w))
- | pr0_zeta : (b:?) ~b=Abst -> (t1,t2:?) (pr0 t1 t2) ->
- (u:?) (pr0 (TTail (Bind b) u (lift (1) (0) t1)) t2)
- | pr0_eps : (t1,t2:?) (pr0 t1 t2) ->
- (u:?) (pr0 (TTail (Flat Cast) u t1) t2).
+ | pr0_beta : (u,v1,v2:?) (pr0 v1 v2) -> (t1,t2:?) (pr0 t1 t2) ->
+ (pr0 (TTail (Flat Appl) v1 (TTail (Bind Abst) u t1))
+ (TTail (Bind Abbr) v2 t2))
+ | pr0_upsilon: (b:?) ~b=Abst -> (v1,v2:?) (pr0 v1 v2) ->
+ (u1,u2:?) (pr0 u1 u2) -> (t1,t2:?) (pr0 t1 t2) ->
+ (pr0 (TTail (Flat Appl) v1 (TTail (Bind b) u1 t1))
+ (TTail (Bind b) u2 (TTail (Flat Appl) (lift (1) (0) v2) t2)))
+ | pr0_delta : (u1,u2:?) (pr0 u1 u2) -> (t1,t2:?) (pr0 t1 t2) ->
+ (w:?) (subst0 (0) u2 t2 w) ->
+ (pr0 (TTail (Bind Abbr) u1 t1) (TTail (Bind Abbr) u2 w))
+ | pr0_zeta : (b:?) ~b=Abst -> (t1,t2:?) (pr0 t1 t2) ->
+ (u:?) (pr0 (TTail (Bind b) u (lift (1) (0) t1)) t2)
+ | pr0_epsilon: (t1,t2:?) (pr0 t1 t2) ->
+ (u:?) (pr0 (TTail (Flat Cast) u t1) t2).
+
+(*#* #stop file *)