Page 728 of 800
| 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 |