Inductive Types Exercises

Thursday 6/27

1. Write the inductive principles for
   • Inductive bool:Set := true:bool | false:bool.
   • Inductive Tree:Set := Leaf | Node:nat → Tree → Tree → Tree.
2. Given
   Inductive Myst[n:nat]:Set := myst:(p:nat) ((plus p p) = n) → (Myst n).
   We have τ:(Myst(S(S 0))). What does the normal form of τ look like?