Spracherkennung für: .out vermutete Sprache: Unknown {[0] [0] [0]} [Methode: Schwerpunktbildung, einfache Gewichte, sechs Dimensionen]
eq_rect :
forall {A : Type} {x : A} (P : A -> Type),
P x -> forall {y : A}, x = y -> P y
eq_rect is not universe polymorphic
Arguments eq_rect {A}%_type_scope {x} P%_function_scope f {y} e
(where some original arguments have been renamed)
eq_rect is transparent
Expands to: Constant Corelib.Init.Logic.eq_rect
Declared in library Corelib.Init.Logic, line 378, characters 0-115
[Dauer der Verarbeitung: 0.15 Sekunden, vorverarbeitet 2026-06-04]
