DEFINITION sn3_pr2_intro()
TYPE =
       ∀c:C.∀t1:T.(∀t2:T.((eq T t1 t2)→∀P:Prop.P)→(pr2 c t1 t2)→(sn3 c t2))→(sn3 c t1)
BODY =
Show proof