proposition: Lemma or_aux_correct : forall c2, interp rho (or_aux c2) = interp rho (l1::c1) || interp rho c2.
proof: Proof. induction c2;simpl. rewrite orb_false_r;trivial. generalize (compare_spec' l1 a);destruct (l1 ?= a);intros H;simpl. rewrite H;destruct (Lit.interp rho a);trivial. rewrite !orb_false_l, or_correct;trivial. rewrite or_correct;simpl;rewrite orb_assoc;trivial. rewrite IHc2;simpl. destruct (Lit.interp rho a);simpl;trivial. rewrite orb_true_r;trivial. Qed.
imports: List Bool Int63 Psatz Ring63 PArray Misc Ring