proposition: Lemma bpermut_ok : bpermut = true <-> permut build_pi.
proof: Proof. unfold bpermut, permut. apply forallb_ok_fintype. 2: hyp. intro f. apply bforall_lt_ok. intro x. rewrite build_pi_ok. apply mem_ok. apply beq_nat_ok. Qed.
imports: CoLoR(LogicUtil ATrs ListUtil NatUtil VecUtil SN BoolUtil RelUtil ListNodup VecFilterPerm ARelation ACompat NaryFunction BoundNat ListDec)