Commit 86b184af by Ralf Jung

docs: strengthen equality elimination to match what we have in Coq

parent 7a2b2c6a
 ... @@ -208,8 +208,8 @@ This is entirely standard. ... @@ -208,8 +208,8 @@ This is entirely standard. {\prop \proves \propC} {\prop \proves \propC} \and \and \infer[Eq] \infer[Eq] {\prop \proves \propB \\ \prop \proves \term =_\type \term'} {\vctx,\var:\type \proves \wtt\propB\Prop \\ \vctx\mid\prop \proves \propB[\term/\var] \\ \vctx\mid\prop \proves \term =_\type \term'} {\prop \proves \propB[\term'/\term]} {\vctx\mid\prop \proves \propB[\term'/\var]} \and \and \infer[Refl] \infer[Refl] {} {} ... @@ -264,7 +264,7 @@ This is entirely standard. ... @@ -264,7 +264,7 @@ This is entirely standard. {\vctx\mid\prop \proves \All \var :\type. \propB \\ {\vctx\mid\prop \proves \All \var :\type. \propB \\ \vctx \proves \wtt\term\type} \vctx \proves \wtt\term\type} {\vctx\mid\prop \proves \propB[\term/\var]} {\vctx\mid\prop \proves \propB[\term/\var]} \and \\ \infer[\$\exists\$I] \infer[\$\exists\$I] {\vctx\mid\prop \proves \propB[\term/\var] \\ {\vctx\mid\prop \proves \propB[\term/\var] \\ \vctx \proves \wtt\term\type} \vctx \proves \wtt\term\type} ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!