Induction priniciple for Elmo

elmo.v

Require Import Arith.
Require Import Bool.
Require Import List.


Definition n : Set := nat.
Definition k : Set := nat.

Inductive Label : Set := 
 | Receive : Label
 | Send : Label.

Inductive Prestate : Type := 
 | Cprestate (_:list Observation)
with Observation : Type := 
 | Cobservation (Label5:Label) (Premessage5:Premessage) (n5:n)
with Premessage : Type := 
 | Cpremessage (Prestate5:Prestate) (n5:n).
(** induction principles *)
Section Premessage_Observation_Prestate_rect.

Variables
  (P_Observation : Observation -> Prop)
  (P_Prestate : Prestate -> Prop)
  (P_Premessage : Premessage -> Prop)
  (P_list_Observation : list Observation -> Prop).

Hypothesis
  (H_Cpremessage : forall (Prestate5:Prestate), P_Prestate Prestate5 -> forall (n5:n), P_Premessage (Cpremessage Prestate5 n5))
  (H_Cobservation : forall (Label5:Label), forall (Premessage5:Premessage), P_Premessage Premessage5 -> forall (n5:n), P_Observation (Cobservation Label5 Premessage5 n5))
  (H_Cprestate : forall (Observation_list:list Observation), P_list_Observation Observation_list -> P_Prestate (Cprestate Observation_list))
  (H_list_Observation_nil : P_list_Observation nil)
  (H_list_Observation_cons : forall (Observation0:Observation), P_Observation Observation0 -> forall (Observation_l:list Observation), P_list_Observation Observation_l -> P_list_Observation (cons Observation0 Observation_l)).

Fixpoint Prestate_ott_ind (n:Prestate) : P_Prestate n :=
  match n as x return P_Prestate x with
  | (Cprestate Observation_list) => H_Cprestate Observation_list (((fix Observation_list_ott_ind (Observation_l:list Observation) : P_list_Observation Observation_l := match Observation_l as x return P_list_Observation x with nil => H_list_Observation_nil | cons Observation1 xl => H_list_Observation_cons Observation1(Observation_ott_ind Observation1)xl (Observation_list_ott_ind xl) end)) Observation_list)
end
with Observation_ott_ind (n:Observation) : P_Observation n :=
  match n as x return P_Observation x with
  | (Cobservation Label5 Premessage5 n5) => H_Cobservation Label5 Premessage5 (Premessage_ott_ind Premessage5) n5
end
with Premessage_ott_ind (n:Premessage) : P_Premessage n :=
  match n as x return P_Premessage x with
  | (Cpremessage Prestate5 n5) => H_Cpremessage Prestate5 (Prestate_ott_ind Prestate5) n5
end.

End Premessage_Observation_Prestate_rect.