proposition: Lemma bvalid_ok : bvalid = true <-> valid.
proof: Proof. unfold valid, bvalid. apply forallb_ok_fintype. 2: hyp. intro f. rewrite orb_eq, beq_nat_ok, bgt_nat_ok. lia. Qed.
imports: CoLoR(ATrs NatUtil BoolUtil VecUtil ListUtil LogicUtil RelUtil SN ACompat ARelation EqUtil)