proposition: Lemma isempty_1: forall n N, isempty N = true -> In n N -> False.
proof: Proof. unfold isempty, In; intros. destruct N as [[l|] [h|]]; try discriminate. apply Z.ltb_lt in H. cbn in H0. lia. Qed.
imports: Coq(ZArith Psatz Bool String List FMaps) Coq(FunctionalExtensionality) CDF(Sequences IMP)