すいません。上のヤツだと
ＬＫにおいて式Ａ、Ｂ→Ｃ、Ｄと→Ａ∧Ｂ⊃Ｃ∨Ｄが同値(＃)使ってます。
本当はでもＬＫで→Ａが証明可能→ＡがＨｑで証明可能示せばいいので＃は必要ないです。

＞＞262表記方まわりの問題になっちゃいそうなのはよくわかるんですがその原因が掴めないのでわけわかりません。
っていうか普通に考えてこんな技法許されるはずないですよね？
なのにできた気になるのが不思議。