From 579681f104d7dc482c1ab02b31d04805ea3e3724 Mon Sep 17 00:00:00 2001
From: Xuanrui Qi <me@xuanruiqi.com>
Date: Wed, 12 Jun 2019 16:51:19 -0700
Subject: [PATCH] Added section about axioms used.

---
 README.md | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/README.md b/README.md
index ba5a2f8..af875fd 100644
--- a/README.md
+++ b/README.md
@@ -38,6 +38,12 @@ Or, if opam is installed, do:
 
 opam takes care of the dependencies.
 
+# External Axioms
+
+We do not explicitly introduce any additional axioms. However, [dynamic_dependent_program.v](dynamic_dependent_program.v) and (to a lesser 
+extent) [dynamic_dependent_tactic.v](dynamic_dependent_tactic.v) uses the `Program` framework and thus implicitly depends on `Coq.Logic.JMEq.JMEq_eq`, 
+which is in turn equivalent to Streicher's Axiom K (i.e., dependent pattern matching).
+
 # Accompanying material
 
 - Most recent [draft paper](201903/compact-20190331.pdf) ([arXiv version](https://arxiv.org/pdf/1904.02809.pdf))