proposition: Lemma test_subst: ((fun f => 0 = 1) true) -> forall x y:nat, forall a b: bool, forall z:nat, 0 <= 1 -> x = z -> (0%Z <= 1%Z)%Z -> x <= y -> x = y -> (0 < 1 -> 1<0) -> 0 < z -> True.
proof: Proof. intros ; { substHyp }. lazymatch reverse goal with | H: y <= y |- True => idtac | _ => fail "test failed!" end. exact I. Qed.
imports: Arith ZArith LibHyps.LibHyps List