Theorem: LoVe.abc_bc_again (LoVe/Lectures/LoVe08_Metaprogramming_Demo.lean)

State before:
a b c : Prop
h : a ∧ b ∧ c
⊢ b ∧ c
Tactic:
destruct_and h
State after:
no goals