From ab21581a911cc858b2e38822e3094068520fde83 Mon Sep 17 00:00:00 2001
From: "Jeremy G. Siek" <jeremy.siek@gmail.com>
Date: Wed, 16 Oct 2024 15:18:11 -0400
Subject: [PATCH] ref for proof instantiation

---
 doc/Reference.md | 27 +++++++++++++++++++++++++++
 1 file changed, 27 insertions(+)

diff --git a/doc/Reference.md b/doc/Reference.md
index 4f3d49d..47cfb50 100644
--- a/doc/Reference.md
+++ b/doc/Reference.md
@@ -920,6 +920,33 @@ proof ::= "injective" term proof
 UNDER CONSTRUCTION
 
 
+## Instantiation (Proof)
+
+```
+proof ::= proof '<' type_list '>'
+proof ::= proof '[' term_list ']'
+```
+
+Use square brackets `[` and `]` to instantiate an `all` formula with 
+terms and use angle brackets `<` and `>` to instantiate an `all`
+formula with types.
+
+Example:
+
+<!-- {.deduce #instantiate_proof_example} -->
+```
+theorem instantiate_proof_example: length(node(42, empty)) = 1
+proof
+  have X: all T:type. all x:T. length(node(x, empty)) = 1 by {
+    arbitrary T:type arbitrary x:T
+    definition {length, length, operator+, operator+}
+  }
+  conclude length(node(42, empty)) = 1
+    by X<Nat>[42]
+end
+```
+
+
 ## Instantiation (Term)
 
 ```