proposition: Lemma isIn_1: forall n N, In n N -> isIn n N = true.
proof: Proof. unfold In, isIn; intros. destruct N; auto. apply Z.leb_le; auto. Qed.
imports: Coq(ZArith Psatz Bool String List FMaps) Coq(FunctionalExtensionality) CDF(Sequences IMP)