proposition: Lemma bnon_dup_ok : bnon_dup = true <-> non_dup build_pi.
proof: Proof. unfold bnon_dup, non_dup. apply forallb_ok_fintype. 2: apply Fs_ok. intro f. rewrite build_pi_ok. apply bnodup_ok. apply beq_nat_ok. Qed.
imports: CoLoR(LogicUtil ATrs ListUtil NatUtil VecUtil SN BoolUtil RelUtil ListNodup VecFilterPerm ARelation ACompat NaryFunction BoundNat ListDec)