proposition: Lemma hold_eOR : forall k r1 r2, hold k (eOR k r1 r2) <-> (hold k r1 \/ hold k r2).
proof: Proof. intros k; destruct k ; simpl. - intros. apply iff_refl. - apply orb_true_iff. Qed.
imports: List Refl Bool Relation_Definitions Setoid