|Page 727 of 800||Search internet|
Origin: check. Landing-place: diagnose.
Curry-seqop used on unfit argument: R
The Curry sequent operator applied to a sequent yields where is meta-conjunction and is meta-implication. The 'Curry-seqop used on unfit argument' indicates that the conclusion of the sequent did not have form . The error may indicate an error in the proof or a bug in a tactic.
|Page 727 of 800||Search logiweb.eu|