proposition: Lemma test_autorename_failing2: 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. intros /n. test x (nat). test y (nat). test H (((fun _ : bool => x = y) true)). test h_le_0_1_ (0 <= 1). test h_le_0_1_0 ((0 <= 1)%Z). test h_le_x_y_ (x <= y). test h_eq_x_y_ (x = y). test h_impl_lt_1_0_ (0 < 1 -> 1 < 0). test h_lt_0_z_ (0 < z). exact I. Qed.
imports: Arith ZArith LibHyps.LibHyps List