proposition: Lemma insert_correct : forall rho (Hwf:Valuation.wf rho) l1 c, C.interp rho (insert 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. destruct (Lit.interp rho a);simpl in *;auto. generalize (Lit.lxor_neg l1 a);destruct (l1 lxor a =? 1);intros;trivial. rewrite C.interp_true;trivial. rewrite H0, Lit.interp_neg;trivial;destruct (Lit.interp rho a);trivial. generalize (Lit.lxor_neg l1 a);destruct (l1 lxor a =? 1);intros. rewrite C.interp_true;trivial. rewrite H0, Lit.interp_neg;trivial;destruct (Lit.interp rho a);trivial. simpl;rewrite orb_assoc,(orb_comm (Lit.interp rho l1)),<-orb_assoc,IHc;trivial. Qed.
imports: List Bool Int63 Psatz Ring63 PArray Misc Ring