Theorem Marketplace

Theorem Details

theorem reverse_reverse {α : Type} (l : List α) : l.reverse.reverse = l := sorry

Bounty: 0.0011 ETH

Status: Closed

Proof

theorem reverse_reverse {α : Type} (l : List α) : l.reverse.reverse = l := by induction l with | nil => rfl | cons hd tl ih => rw [List.reverse_cons, List.reverse_append, ih]; rfl

Back to Bounties