proposition: Lemma join_1: forall n N1 N2, In n N1 -> In n (join N1 N2).
proof: Proof. unfold In, join; intros; cbn. destruct N1, N2; try tauto. destruct (Z.eqb_spec n0 n1); auto. Qed.
imports: Coq(ZArith Psatz Bool String List FMaps) CDF(Sequences IMP)