Page 722 of 800
| Page 722 of 800 | Search internet |
Origin: check. Landing-place: diagnose.
Init-seqop used on non-meta term: x
The Init sequent operator applied to a term x yields the sequent 
which states that x is provable if x is provable. The operation requires x to be wellformed. The error may indicate an error in the proof or a bug in a tactic.
| Page 722 of 800 | Search logiweb.eu |