S-design-memo-1

Using theorems

When the users use theorems, they just copy the statement in their proof

code:s

-- Use th0

(1) for all a { a = a }

After copying it into the proof, substitute terms into variables to make it convenient for the proof

Let's have many inference rules in addition to LK

Maybe let's make the users define new inference rules.