DEFINITION pr3_confluence()
TYPE =
       c:C.t0:T.t1:T.(pr3 c t0 t1)t2:T.(pr3 c t0 t2)(ex2 T λt:T.pr3 c t1 t λt:T.pr3 c t2 t)
BODY =
Show proof