DEFINITION nf2_pr3_confluence()
TYPE =
       ∀c:C.∀t1:T.(nf2 c t1)→∀t2:T.(nf2 c t2)→∀t:T.(pr3 c t t1)→(pr3 c t t2)→(eq T t1 t2)
BODY =
Show proof