left

left

Coq < Goal A -> A \/ B.
1 subgoal

  ============================
   A -> A \/ B

Unnamed_thm4 < intro.
1 subgoal

  H : A
  ============================
   A \/ B

Unnamed_thm4 < left.
1 subgoal

  H : A
  ============================
   A

Unnamed_thm4 < assumption.
Proof completed.