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.11 Sekunden
(vorverarbeitet)
]
