proposition: Lemma build_pi_ok : forall f, map N_val (build_pi f) = raw_pi f.
proof: Proof. intro. apply build_nat_lts_ok. Qed.
imports: CoLoR(LogicUtil ATrs ListUtil NatUtil VecUtil SN BoolUtil RelUtil ListNodup VecFilterPerm ARelation ACompat NaryFunction BoundNat ListDec)