Lemma zad:
forall a: bool,
forall b: bool,
forall c: bool,
forall d: bool,
forall H: a = true -> c = false \/ d = false,
forall H0: a = b,
forall H1: d = false -> c = false,
forall H2: b = true,
c=false.

Proof.
intros.
rewrite H2 in H0.
apply H in H0.
decompose [or] H0.
assumption.
apply H1.
assumption.
Qed.