proposition: Lemma test_revertHyp: 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 ; { revertHyp }. intros ; {< revertHyp }. testg (forall x y : nat, (fun _ : bool => x = y) true -> bool -> bool -> forall z : nat, 0 <= 1 -> (0 <= 1)%Z -> x <= y -> x = y -> (0 < 1 -> 1 < 0) -> 0 < z -> True). intros. exact I. Qed.
imports: Arith ZArith LibHyps.LibHyps List