forallb_forall.v

 Lemma monotone_operator_w : forall k, Fixpoints.mon (W k).
  Proof.
    intros k. unfold Fixpoints.mon. intros p1 p2 H.
    unfold W. unfold Fixpoints.pred_subset in *.
    intros a H1. apply andb_true_iff in H1.
    apply andb_true_iff. destruct H1 as [H2 H3].
    split. assumption. unfold mp in *.
    apply forallb_forall.
    
Goal: 
  k : nat
  p1, p2 : Fixpoints.pred (cand * cand)
  H : forall a : cand * cand, p1 a = true -> p2 a = true
  a : cand * cand
  H2 : el k a = true
  H3 : forallb (mpf k a p1) cand_all = true
  ============================
  forall x : cand, In x cand_all -> mpf k a p2 x = true

When I am applying forallb_for in H3, I am getting Error: Statement without assumptions.

https://github.com/mukeshtiwari/formalized-voting/blob/master/Schulze_Dirk.v#L356

Using specialize (forallb_forall _ cand_all H3).

I am getting Error: Illegal application (Non-functional construction):
The expression "forallb_forall ?b cand_all" of type
"forallb ?b cand_all = true <-> (forall x : cand, In x cand_all -> ?b x = true)"
cannot be applied to the term
"H3" : "forallb (mpf k a p1) cand_all = true"