proposition: Lemma build_nat_lts_ok : forall n l (h : forallb (bgt_nat n) l = true), map N_val (build_nat_lts h) = l.
proof: Proof. induction l; simpl; intros. refl. rewrite IHl. refl. Qed.
imports: CoLoR(LogicUtil ATrs ListUtil NatUtil VecUtil SN BoolUtil RelUtil ListNodup VecFilterPerm ARelation ACompat NaryFunction BoundNat ListDec)