Library UniMath.MoreFoundations.Bool
Require Import UniMath.Foundations.Init.
Require Import UniMath.Foundations.Sets.
Definition andb : bool -> bool -> bool.
Show proof.
Definition orb : bool -> bool -> bool.
Show proof.
Definition implb : bool -> bool -> bool.
Show proof.
Lemma andb_is_associative :
∏ b1 b2 b3 : bool, andb (andb b1 b2) b3 = andb b1 (andb b2 b3).
Show proof.
intros; induction b1; induction b2; induction b3; reflexivity.
Lemma orb_is_associative :
∏ b1 b2 b3 : bool, orb (orb b1 b2) b3 = orb b1 (orb b2 b3).
Show proof.
intros; induction b1; induction b2; induction b3; reflexivity.
Lemma andb_is_commutative :
∏ b1 b2 : bool, andb b1 b2 = andb b2 b1.
Show proof.
intros; induction b1; induction b2; reflexivity.
Lemma orb_is_commutative :
∏ b1 b2 : bool, orb b1 b2 = orb b2 b1.
Show proof.
intros; induction b1; induction b2; reflexivity.