intro

intro

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

Unnamed_thm < intro.
1 subgoal
  
  H : A
  ============================
   A

Unnamed_thm < assumption.
Proof completed.

* はてなダイアリーキーワード:intro