lambda_induction_in_coq.v

Set Universe Polymorphism.

Set Primitive Projections.
Record ssig (A : Type) (P : A -> SProp) : Type := { l : A; r : P l }.

Definition C_Bool : Type := forall A, A -> A -> A.
Definition c_true : C_Bool := fun A x y => x.
Definition c_false : C_Bool := fun A x y => y.

Definition I_Bool (c_b : C_Bool) : SProp :=
  forall P : C_Bool -> SProp, P c_true -> P c_false -> P c_b.
Definition i_true : I_Bool c_true := fun A x y => x.
Definition i_false : I_Bool c_false := fun A x y => y.

Definition Bool : Type := ssig C_Bool I_Bool.
Definition true : Bool := {| l := c_true; r := i_true |}.
Definition false : Bool := {| l := c_false; r := i_false |}.

Theorem ind_bool b : forall P : Bool -> SProp, P true -> P false -> P b.
  intros P p_t p_f.
  destruct b as [b_l b_r].
  refine (b_r (fun x_l => forall x_r : I_Bool x_l, _) _ _ b_r).
  intros x_r; exact p_t.
  intros x_r; exact p_f.
Qed.