proposition: Theorem beq_id_true_iff : forall x y : id, beq_id x y = true <-> x = y.
proof: Proof. intros [n1] [n2]. unfold beq_id. destruct (string_dec n1 n2). - subst. split. reflexivity. reflexivity. - split. + intros contra. inversion contra. + intros H. inversion H. subst. destruct n. reflexivity. Qed.
imports: Coq.Arith.Arith Coq.Bool.Bool Coq.Strings.String Coq.Logic.FunctionalExtensionality