Commit 6835f6f2 authored by Florian Rabe's avatar Florian Rabe

no message

parent 6fda40ee
......@@ -5,6 +5,7 @@ import objects._
import checking._
import info.kwarc.mmt.api.symbols.OMLReplacer
import info.kwarc.mmt.lf._
import lf.PropositionsITP
import lf.Proofs
import lf.Types
......
......@@ -14,7 +14,7 @@ theory UniversalQuantificationNDI =
theory UniversalQuantificationNDE =
include ?UniversalQuantification❙
forallE : {P,X} ⊦ ∀ P ⟶ ⊦ (P X)❘# 2 forallE 3❘role ForwardRule❙
forallE : {P,X} ⊦ ∀ P ⟶ ⊦ (P X)❘# 3 forallE 2❘role ForwardRule❙
theory UniversalQuantificationND =
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment