Fixed mistake in Equal_elim and proof of rpathcomp_comp

1 files changed, 1 insertions, 1 deletions

diff --git a/Equal.thy b/Equal.thy
index bd7dd93..11a966b 100644
--- a/Equal.thy
+++ b/Equal.thy
@@ -37,7 +37,7 @@ and
     \<And>x. x: A \<Longrightarrow> f(x) : C(x)(x)(refl x);
     x: A;
     y: A;
-    p: a =\<^sub>A b
+    p: x =\<^sub>A y
     \<rbrakk> \<Longrightarrow> ind\<^sub>=(f)(p) : C(x)(y)(p)"
 and
   Equal_comp: "\<lbrakk>