INDUCTIVE DEFINITION sn3 () [ :C ]
OF ARITY T→Prop
BUILT FROM:
     sn3_sing: ∀t1:T.(∀t2:T.((eq T t1 t2)→∀P:Prop.P)→(pr3 c t1 t2)→(sn3 c t2))→(sn3 c t1)