|Page 728 of 800||Search internet|
Origin: check. Landing-place: diagnose.
Uncurry-seqop used on unfit argument: R
The Uncurry sequent operator applied to a sequent yields where is meta-conjunction and is meta-implication. The 'Uncurry-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 728 of 800||Search logiweb.eu|