Inductive month : Set := January | February | March | April | May | June | July | August | September | October | November | December. Inductive season : Set := Spring | Summer | Fall | Winter. Definition month_season := month_rec (fun _ => season) Winter Winter Spring Spring Spring Summer Summer Summer Fall Fall Fall Winter. Definition month_season2 (m:month) : season := match m with January => Winter | February => Winter | March => Spring | April => Spring | May => Spring | June => Summer | July => Summer | August => Summer | September => Fall | October => Fall | November => Fall | December => Winter end. Theorem month_season_eq : forall m : month, month_season m = month_season2 m. Proof. intro m. unfold month_season; unfold month_season2. unfold month_rec. unfold month_rect. case m; trivial. Qed.