Theorem: LoVe.BackwardProofs.proj_fst (LoVe/Labs/Lab2Solution.lean)

State before:
a : Prop
⊢ a → a → a
Tactic:
intro ha ha'
State after:
a : Prop
ha ha' : a
⊢ a

State before:
a : Prop
ha ha' : a
⊢ a
Tactic:
exact ha
State after:
no goals