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