Theorem: LoVe.BackwardProofs.fst_of_two_props (LoVe/Lectures/LoVe03_BackwardProofs_Demo.lean)

State before:
⊢ ∀ (a b : Prop), a → b → a
Tactic:
intro a b
State after:
a b : Prop
⊢ a → b → a

State before:
a b : Prop
⊢ a → b → a
Tactic:
intro ha hb
State after:
a b : Prop
ha : a
hb : b
⊢ a

State before:
a b : Prop
ha : a
hb : b
⊢ a
Tactic:
apply ha
State after:
no goals