snd: forall c : c, fst c = 0