proposition: Lemma insert_keep_correct : forall rho (Hwf:Valuation.wf rho) l1 c, C.interp rho (insert_keep l1 c) = C.interp rho (l1 :: c).
proof: Proof. intros rho Hwf l1;induction c;simpl;trivial. generalize (compare_spec' l1 a);destruct (l1 ?= a);intros;subst;simpl;auto. destruct (Lit.interp rho a);simpl in *;auto. rewrite orb_true_r; auto. Qed.
imports: List Bool Int63 Psatz Ring63 PArray Misc Ring