(*#* #caption "confluence with single step reduction: strip lemma" *)
(*#* #cap #cap c, t0, t1, t2, t *)
Theorem pr3_strip : (c:?; t0,t1:?) (pr3 c t0 t1) -> (t2:?) (pr2 c t0 t2) ->
(EX t | (pr3 c t1 t) & (pr3 c t2 t)).
(*#* #caption "confluence with single step reduction: strip lemma" *)
(*#* #cap #cap c, t0, t1, t2, t *)
Theorem pr3_strip : (c:?; t0,t1:?) (pr3 c t0 t1) -> (t2:?) (pr2 c t0 t2) ->
(EX t | (pr3 c t1 t) & (pr3 c t2 t)).