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

State before:
a b c : Prop
hab : a → b
hbc : b → c
⊢ a → c
Tactic:
intro ha
State after:
a b c : Prop
hab : a → b
hbc : b → c
ha : a
⊢ c

State before:
a b c : Prop
hab : a → b
hbc : b → c
ha : a
⊢ c
Tactic:
apply hbc
State after:
a b c : Prop
hab : a → b
hbc : b → c
ha : a
⊢ b

State before:
a b c : Prop
hab : a → b
hbc : b → c
ha : a
⊢ b
Tactic:
apply hab
State after:
a b c : Prop
hab : a → b
hbc : b → c
ha : a
⊢ a

State before:
a b c : Prop
hab : a → b
hbc : b → c
ha : a
⊢ a
Tactic:
apply ha
State after:
no goals