Logiweb diagnose of problemtwo

Up Help

Error in proof of nontriv4 Metageneralization over metavariable that occurs free in some premise: ∀\underline{q}: \underline{p} ⇒ \underline{q} ⊢ ∀\underline{\underline{p}}: ∀\underline{\underline{q}}: nontriv0^{I}^{⊳} ^{∗}^{⊳} @ \underline{\underline{p}} @ \underline{\underline{q}} @ \underline{p} @ \underline{q}^{⊳} ^{⊳} ^{⊳}

The pyk compiler, version 0.grue.20060417+ by Klaus Grue GRD-2006-07-12.UTC:19:00:11.024866 = MJD-53928.TAI:19:00:44.024866 = LGT-4659447644024866e-6