Theorem: MyNat.imp_self (TheoremProvingLean/inductive_types.lean)

State before:
P : Prop
⊢ P → P
Tactic:
intro p
State after:
P : Prop
p : P
⊢ P

State before:
P : Prop
p : P
⊢ P
Tactic:
exact p
State after:
no goals