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