(*#* #caption "confluence with itself: Church-Rosser property" *)
(*#* #cap #cap t0, t1, t2, t *)
Theorem pr1_confluence : (t0,t1:?) (pr1 t0 t1) -> (t2:?) (pr1 t0 t2) ->
(EX t | (pr1 t1 t) & (pr1 t2 t)).
(*#* #caption "confluence with itself: Church-Rosser property" *)
(*#* #cap #cap t0, t1, t2, t *)
Theorem pr1_confluence : (t0,t1:?) (pr1 t0 t1) -> (t2:?) (pr1 t0 t2) ->
(EX t | (pr1 t1 t) & (pr1 t2 t)).