Section Jahreszeiten.

Inductive season: Type :=
  spring: season | summer: season 
 | autumn: season | winter: season.

(* Induktionsprinzip *)
Check season_ind.  (* Überprüfung aller Fälle *)

(* Rekursionsprinzip *)
Check season_rect.  (* Wertetabelle *)

Print season_rect.

Definition num_days:=
season_rect (fun _=>nat)  92 94 90 89 .

Eval compute in num_days.
Eval compute in forall s:season, (fun _ : season => nat) s.

Eval compute in (num_days summer).

Lemma num_days_summer:
(num_days summer) = 94.
Proof.
simpl.
trivial.
Qed.