proposition: Lemma forallb_ok_fintype : forallb f As = true <-> forall x, P x.
proof: Proof. split; intro H. intro x. rewrite <- f_ok. rewrite forallb_forall in H. apply H. apply As_ok. rewrite forallb_forall. intros x hx. rewrite f_ok. apply H. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)