split

split


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

Unnamed_thm0 < intros.
1 subgoal
  
  H : A
  H0 : B
  ============================
   A /\ B

Unnamed_thm0 < split.
2 subgoals
  
  H : A
  H0 : B
  ============================
   A

subgoal 2 is:
 B

Unnamed_thm0 < assumption.
1 subgoal
  
  H : A
  H0 : B
  ============================
   B

Unnamed_thm0 < assumption.
Proof completed.