(P: Prop).P))) \to ((pr3 c t1 t2) \to (sn3 c t2))))) \to (sn3 c t1)).
let rec sns3 (c: C) (ts: TList) on ts: Prop \def match ts with [TNil
(P: Prop).P))) \to ((pr3 c t1 t2) \to (sn3 c t2))))) \to (sn3 c t1)).
let rec sns3 (c: C) (ts: TList) on ts: Prop \def match ts with [TNil