proposition: Theorem beq_id_false_iff : forall x y : id, beq_id x y = false <-> x <> y.
proof: Proof. intros x y. rewrite <- beq_id_true_iff. rewrite not_true_iff_false. reflexivity. Qed.
imports: Coq.Arith.Arith Coq.Bool.Bool Coq.Strings.String Coq.Logic.FunctionalExtensionality