proposition: Lemma bweight_inj_ok : bweight_inj = true <-> (forall f g, weight f = weight g -> f = g).
proof: Proof. unfold bweight_inj. apply forallb_ok_fintype. 2: hyp. intro f. apply forallb_ok_fintype. 2: hyp. intro g. unfold implb. case_eq (beq_nat (weight f) (weight g)). rewrite beq_nat_ok, beq_symb_ok. tauto. rewrite (beq_ko beq_nat_ok). tauto. Qed.
imports: CoLoR(EqUtil ListUtil LogicUtil) Coq(DecidableType) CoLoR(NatUtil BoolUtil)