proposition: Lemma eqbool_irrelevance : forall (b : bool) (h1 h2 : b = true), h1 = h2.
proof: Proof. assert (forall (h : true = true), refl_equal true = h). apply (eq_dep_elim bool true (eqbool_dep _ _) (refl_equal _)). intros b. case b. intros h1 h2. now rewrite <- (H h1). intros h. discriminate h. Qed.
imports: Coq(ZArith Lia Zquot)