blob: d584cf752e6a94908a4ec47137b5966e28e18022 (
plain)
1
2
3
4
5
6
7
8
|
Module Wish11692.
(* Support for let-in in clear dependent *)
Goal forall x : Prop, let z := 0 in let z' : (fun _ => True) x := I in let y := x in y -> True.
Proof. intros x z z' y H. clear dependent x. Show. exact I. Qed.
End Wish11692.
|
