when hypothesis is instantiated, we first generalize the hypothesis

21-190041.v

Theorem instantiated :
forall m:nat,
  m <= 0 -> m = 0.
Proof.
  intros. induction H.
  - reflexivity.
  - subst. Abort.

Theorem generalized :
  forall m n,
  m <= n -> n = 0 -> m = 0.
Proof.
  intros. induction H.
  - assumption.
  - inversion H0.
Qed.


Theorem lt_0_is_0 :
  forall m:nat,
    m <= 0 -> m =0.
Proof.
  intros. specialize(generalized _ _ H eq_refl).
  trivial.
Qed.