Proving path composition. Need to set up the Simplifier to simplify application of object-lambdas to arguments.

1 files changed, 1 insertions, 0 deletions

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."