proposition: Lemma bis_unary_ok : forall (Fs : list Sig) (Fs_ok : forall f, In f Fs), bis_unary Fs = true <-> is_unary.
proof: Proof. intros. apply forallb_ok_fintype. intro. rewrite beq_nat_ok. refl. hyp. Qed.
imports: CoLoR(ATrs VecUtil LogicUtil ListUtil NatUtil VecMax EqUtil RelUtil SN ListMax)