proposition: Lemma Ls_ok : forall f (x : L f), List.In x (Ls f).
proof: Proof. intros f x. unfold Ls. apply (enum_tuple_complete I Is_ok). Qed.
imports: CoLoR(ATrs LogicUtil ListUtil VecUtil BoolUtil EqUtil ASemLab SN NatUtil RelUtil AWFMInterpretation)