proposition: Lemma bvalid_ok : bvalid = true <-> valid.
proof: Proof. unfold bvalid, valid. apply forallb_ok_fintype. 2: hyp. intro f. unfold bvalid_symb. destruct (raw_pi f). rewrite bgt_nat_ok. intuition. inversion H1. subst. auto. intuition. discr. Qed.
imports: CoLoR(ATrs VecUtil LogicUtil ListUtil SN ARelation RelUtil ACompat NatUtil)