Theorem: LoVe.ForwardProofs.nat_exists_double_iden (LoVe/Lectures/LoVe04_ForwardProofs_Demo.lean)

State before:
⊢ double 0 = 0
Tactic:
rfl
State after:
no goals