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

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