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