proposition: Lemma pointwise_variant_diff : forall y, y<> x -> p_v y = f y.
proof: Proof. intros y Hn; unfold p_v; elim (epsilon_spec(inhabits v)(fun w =>(y=x->w=v)/\(y<>x->w=f y))). intuition. exists (f y);split;[intros Habs; elim Hn;auto|auto]. Qed.
imports: Relations Classical ClassicalEpsilon Zwf Compare_dec List ZArith