Definition bor (x y : bool) : bool :=
    match x with
    | true  => true
    | false => if y then true else false
    end.

Definition band (x y : bool) : bool :=
    match x with
    | false => false
    | true  => if y then true else false
    end.

Definition bxor (x y : bool) : bool :=
    match x with
    | true  => if y then false else true
    | false => if y then true  else false
    end.

Definition bnot (x : bool) : bool :=
    match x with
    | true  => false
    | false => true
    end.

Definition bimpl (x y : bool) : bool := bor (bnot x) y.

Definition biff (x y : bool) : bool := band (bimpl x y) (bimpl y x).

Theorem de_morgan_1 : forall (x y : bool), biff (bnot (bor x y)) (band (bnot x) (bnot y)) = true.
Proof.
    intros X Y.
    induction X.
    Focus 1.
    compute.
    reflexivity.
    induction Y.
    Focus 1.
    compute.
    reflexivity.
    compute.
    reflexivity.
Qed.

Corollary de_morgan_2 : forall (x y : bool), biff (bnot (band x y)) (bor (bnot x) (bnot y)) = true.
Proof.
    intros X Y.
    induction X.
    Focus 1.
    induction Y.
    Focus 1.
    compute.
    reflexivity.
    Focus 1.
    compute.
    reflexivity.
    induction Y.
    Focus 1.
    compute.
    reflexivity.
    compute.
    reflexivity.
Qed.