From 86b184afcc56d5ded234d074617bf356dc7614ce Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 7 Oct 2016 10:59:10 +0200
Subject: [PATCH] docs: strengthen equality elimination to match what we have
in Coq
---
docs/base-logic.tex | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/docs/base-logic.tex b/docs/base-logic.tex
index 26bebe1de..9039a5af3 100644
--- a/docs/base-logic.tex
+++ b/docs/base-logic.tex
@@ -208,8 +208,8 @@ This is entirely standard.
{\prop \proves \propC}
\and
\infer[Eq]
- {\prop \proves \propB \\ \prop \proves \term =_\type \term'}
- {\prop \proves \propB[\term'/\term]}
+ {\vctx,\var:\type \proves \wtt\propB\Prop \\ \vctx\mid\prop \proves \propB[\term/\var] \\ \vctx\mid\prop \proves \term =_\type \term'}
+ {\vctx\mid\prop \proves \propB[\term'/\var]}
\and
\infer[Refl]
{}
@@ -264,7 +264,7 @@ This is entirely standard.
{\vctx\mid\prop \proves \All \var :\type. \propB \\
\vctx \proves \wtt\term\type}
{\vctx\mid\prop \proves \propB[\term/\var]}
-\and
+\\
\infer[$\exists$I]
{\vctx\mid\prop \proves \propB[\term/\var] \\
\vctx \proves \wtt\term\type}
--
GitLab