proposition: Lemma resolve_aux_correct : forall rho, (forall c2, interp rho c1 -> interp rho c2 -> interp rho (resolve c1 c2)) -> interp rho (l1 :: c1) -> forall c2, interp rho c2 -> interp rho (resolve_aux c2).
proof: Proof. intros rho resolve_correct Hc1;simpl in Hc1. induction c2;simpl;try discriminate. generalize (compare_spec' l1 a);destruct (l1 ?= a);intros;subst;simpl. simpl in Hc1;destruct (Lit.interp rho l1);simpl in *;auto. generalize (Lit.lxor_neg l1 a);destruct (l1 lxor a =? 1);intros. rewrite or_correct. rewrite H1, Lit.interp_neg in Hc1;trivial;destruct (Lit.interp rho a). simpl in Hc1;rewrite Hc1;trivial. simpl in H0;rewrite H0, orb_true_r;trivial. simpl;destruct (Lit.interp rho l1);simpl;auto. generalize (Lit.lxor_neg l1 a);destruct (l1 lxor a =? 1);intros. rewrite or_correct. rewrite H1, Lit.interp_neg in Hc1;trivial;destruct (Lit.interp rho a). simpl in Hc1;rewrite Hc1;trivial. simpl in H0;rewrite H0, orb_true_r;trivial. simpl;destruct (Lit.interp rho a);simpl;auto. Qed.
imports: List Bool Int63 Psatz Ring63 PArray Misc Ring