proposition: Lemma sort_uniq_correct : forall rho (Hwf:Valuation.wf rho) c, C.interp rho (sort_uniq c) = C.interp rho c.
proof: Proof. intros rho Hwf;induction c;simpl;trivial. rewrite insert_correct;trivial;simpl;rewrite IHc;trivial. Qed.
imports: List Bool Int63 Psatz Ring63 PArray Misc Ring