diff options
Diffstat (limited to 'EqualProps.thy')
| -rw-r--r-- | EqualProps.thy | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/EqualProps.thy b/EqualProps.thy index abb2623..f7a8d91 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -117,7 +117,6 @@ proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p]) fix x assume "x: A" show "refl (q \<bullet> r): (refl x) \<bullet> (q \<bullet> r) =[x =\<^sub>A w] ((refl x) \<bullet> q) \<bullet> r" \<comment> \<open>This requires substitution of *propositional* equality. \<close> - sorry oops |