Tidy up project

* Write README.md
* Add LICENSE
* Clean up some theorems and proofs

1 files changed, 6 insertions, 0 deletions

diff --git a/expr.v b/expr.v
index 11c0737..e770345 100644
--- a/expr.v
+++ b/expr.v
@@ -60,6 +60,12 @@ Instance Maybe_X_Attrset : Maybe X_Attrset := λ e,
   | _ => None
   end.
 
+Instance Maybe_X_V : Maybe X_V := λ e,
+  match e with
+  | X_V v => Some v
+  | _ => None
+  end.
+
 Instance Maybe_B_Nonrec : Maybe B_Nonrec := λ rhs,
   match rhs with
   | B_Nonrec e => Some e