1 2 3 4 5 6 7 8
(* Check Generalize Dependent *) Lemma l1 : let a := 0 in let b := a in forall (c : b = b) (d : True -> b = b), d = d. intros. generalize dependent a. intros a b c d. Abort.