proposition: Lemma init_not_in_nids: not (In init_nid nids).
proof: Proof. intro. unfold init_nid in H. assert (A := below_max_in_nids MaxNId). apply A in H. apply Nat.lt_irrefl in H. assumption. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)