proposition: Lemma decidable_pred_pred : forall a : Data, {fun_or Data pred pred a = true} + {fun_or Data pred pred a = false}.
proof: Proof. unfold fun_or in |- *. intro a. generalize (decidable_predicate a). intro H. elim H. intro y. rewrite y. simpl in |- *. auto. intro y. rewrite y. simpl in |- *. auto. Qed.
imports: List fifo table reduce