From 14a5e50ab3ed54767a4432333642e9069ffa9109 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sat, 30 Jun 2018 19:21:58 +0200
Subject: Proving path composition. Need to set up the Simplifier to simplify
 application of object-lambdas to arguments.

---
 Prod.thy | 1 +
 1 file changed, 1 insertion(+)

(limited to 'Prod.thy')

diff --git a/Prod.thy b/Prod.thy
index 5f0d272..162b2e6 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -60,6 +60,7 @@ text "The type rules should be able to be used as introduction and elimination r
 
 lemmas Prod_rules [intro] = Prod_form Prod_intro Prod_elim Prod_comp Prod_uniq
 lemmas Prod_form_conds [elim] = Prod_form_cond1 Prod_form_cond2
+lemmas Prod_simps [simp] = Prod_comp Prod_uniq
 
 text "Nondependent functions are a special case."
 
-- 
cgit v1.2.3