LetP.v
(*****************************************************************************)
(* *)
(* Buchberger : let construct *)
(* *)
(* Laurent Thery March 98 (revised Mai 98) *)
(* *)
(*****************************************************************************)
Definition
LetP: (A, B:Set) (h:A) ((u:A) u =h ->B) ->B.
Intros A B h H'.
Apply H' with u := h.
Auto.
Defined.
29/06/100, 12:53