Funky tree

With sound and complete apologies to the authors of the song Funky Town:

Inductive funky_tree : Type :=
  Nat : nat -> funky_tree
| Bool : bool -> funky_tree
| String : string -> funky_tree
| Singleton : funky_tree -> funky_tree
| Pair : funky_tree -> funky_tree -> funky_tree
| Triple : funky_tree -> funky_tree -> funky_tree -> funky_tree.

Here we go:

Gotta make a move for a proof that's right for me
Proof to keep me movin', keep me provin' with more energy

Well, I talk about tic, walk around lit
Gawk about wit, poke around bits

Poke around, gawk about
Talk about provin'

Gotta prove on
Gotta prove on
Gotta prove on

A-won't you show me a funky tree?
Won't you make me a funky tree?
Won't you shape me a funky tree?
Won't you shake me a funky tree?

Won't you show me a funky proof?
Won't you make me a funky proof?
Won't you bake me a funky proof?
Won't you snap me a Qed?

etc. (you get the drift)

Version

Created [16 Feb 2024]