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