Spracherkennung für: .out vermutete Sprache: Unknown {[0] [0] [0]} [Methode: Schwerpunktbildung, einfache Gewichte, sechs Dimensionen]
File "./output/bug6404.v", line 7, characters 7-11:
The command has indeed failed with message:
The term "I" has type "True"
which should be Set, Prop or Type.
In nested Ltac calls to "c", "abs", "transparent_abstract (tactic3)",
"b", "a", "pose (I : I)" and "(I : I)", last term evaluation failed.
[Dauer der Verarbeitung: 0.12 Sekunden, vorverarbeitet 2026-04-26]
