intros

intros

Coq < Goal A -> B -> A.
1 subgoal
  
  ============================
   A -> B -> A

Unnamed_thm2 < intros.
1 subgoal
  
  H : A
  H0 : B
  ============================
   A

Unnamed_thm2 < assumption.
Proof completed.