import MyNat.Definition

Tactic intros

The intros tactic is like intro only it can introduce multiple hypotheses at once.

Usage intros h₁ h₂ h₃ ....