proposition: Lemma isIn_1: forall n v, In n v -> isIn n v = true.
proof: Proof. unfold In, isIn; intros. apply andb_true_intro; split; apply Zinf.isIn_1; tauto. Qed.
imports: Coq(ZArith Psatz Bool String List FMaps) Coq(FunctionalExtensionality) CDF(Sequences IMP)