eq (f 0) 0 : Prop