Quellcodebibliothek
Statistik
Leitseite
products
/
Sources
/
formale Sprachen
/
Roqc
/
test-suite
/
output
/ (
Beweissystem des Inria
Version 9.1.0
©
) Datei vom 15.8.2025 mit Größe 106 B
Quelle bug_13238.out Sprache: unbekannt
Ltac t1 x := replace (x x) with (x x)
Ltac t2 x := case : x
Ltac t3 := by move ->
Ltac t4 := congr True
[ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet)
]
2026-04-04