Commit d0d2881c authored by Florian Rabe's avatar Florian Rabe

no message

parent 1b8a8ad9
namespace latin:/❚
theory PropositionsITP =
proof # block proof 1;…❙
hence # %n L1T by 2❙
suffices # %n 1❙
use # use 1,… ❙
theory PLITP =
include ?PropositionsITP❙
assume # %n L1T❙
cases # %n 1,…❙
theory SFOLITP =
include ?PLITP❙
fix # %n L1T❙
theory Test : ?SFOLITP =
include ?FOLEQND❙
test : {A: term ⟶ prop} ⊦ ∀ [x] A x ⇒ A x❘
= [A] proof fix x; assume a; use a❙
\ No newline at end of file
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