complement_set.v

  Definition pred (A: Type) := A -> bool.

  (* subset relation on boolean predicates *)
  Definition pred_subset {A: Type} (p1 p2: pred A) :=
    forall a: A, p1 a = true -> p2 a = true.

  (* extensional equality of boolean predicates *)
  Definition pred_eeq {A: Type} (p1 p2: pred A) :=
    pred_subset p1 p2 /\ pred_subset p2 p1.
    
  Definition complement {A : Type} p : pred A := fun x => negb (p x).
  
    Lemma eeq_complement : forall (A : Type) (p q : pred A),
      pred_eeq p q -> pred_eeq (complement p) (complement q).
  Proof.
    intros A p q H. unfold pred_eeq in *. unfold pred_subset in *.
    destruct H. unfold complement. split. intros a Hn. apply negb_true_iff.
    apply negb_true_iff in Hn.

Goal
  A : Type
  p, q : pred A
  H : forall a : A, p a = true -> q a = true
  H0 : forall a : A, q a = true -> p a = true
  a : A
  Hn : p a = false
  ============================
  q a = false

subgoal 2 (ID 329) is:
 forall a : A, negb (q a) = true -> negb (p a) = true