decompose

decompose

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

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

Unnamed_thm0 < decompose [and] H.
1 subgoal
  
  H : A /\ B
  H0 : A
  H1 : B
  ============================
   A

Unnamed_thm0 < assumption.
Proof completed.