proposition: Lemma test_autorename_failing: forall x y:nat, ((fun f => x = y) true) -> forall a b: bool, forall z:nat, 0 <= 1 -> (0%Z <= 1%Z)%Z -> x <= y -> x = y -> (0 < 1 -> 1<0) -> 0 < z -> True.
proof: Proof. Fail intros /n!. intros ; { autorename }. test H ((fun _ : bool => x = y) true). auto. Qed.
imports: Arith ZArith LibHyps.LibHyps List