Abstracting the function

  Definition bool_in (p: (cand * cand)%type) (l: list (cand * cand)%type) :=
    existsb (fun q => (andb (cand_eqb (fst q) (fst p))) ((cand_eqb (snd q) (snd p)))) l. 
    
  Definition el (k: nat) (p: (cand * cand)%type) := Compare_dec.leb (edge (fst p) (snd p)) k.

  Lemma edge_prop : forall a b k, el k (a, b) = true -> edge a b <= k.
  Proof.
    intros a b k H; unfold el in H; simpl in H;
    apply leb_complete in H; assumption.
  Qed.

  Lemma boolin_prop :  forall a b l, bool_in (a, b) l = true -> In (a, b) l.
  Proof. Admitted.
  
  Lemma fold_left_true :
    forall (p : cand * cand) (l : list (cand * cand)) (k : nat), 
    fold_left (fun (x : bool) (b : cand)
               => andb x (orb (bool_in (b, snd p) l)
                             (el k (fst p, b)))) cand_all true = true ->
    forall c , (bool_in (c, snd p) l) = true \/  (el k (fst p, c)) = true.
  Proof. intros.
  
  
  p : cand * cand
  l : list (cand * cand)
  k : nat
  H : fold_left (fun (x : bool) (b : cand) => x && (bool_in (b, snd p) l || el k (fst p, b)))
        cand_all true = true
  c : cand
  ============================
   bool_in (c, snd p) l = true \/ el k (fst p, c) = true