% hol-1.0.elf

sample : |- true ==> true  = disch ([u] u).