Definition sig_fst {A B} {p q : {x : A | B x}} (H : p = q)
  : proj1_sig p = proj1_sig q :=
  eq_rect _ (fun z => proj1_sig p = proj1_sig z) eq_refl _ H.

Definition sig_snd {A B} {p q : {x : A | B x}} (H : p = q)
  : eq_rect _ B (proj2_sig p) _ (sig_fst H) = proj2_sig q :=
  match H with
  | eq_refl => eq_refl
  end.

Lemma sig_ext {A B} (p q : {x : A | B x})
  (H1 : proj1_sig p = proj1_sig q)
  (H2 : eq_rect _ B (proj2_sig p) _ H1 = proj2_sig q)
  : p = q.
  destruct p, q; simpl in *.
  destruct H1, H2; simpl in *.
  reflexivity.
Defined.

Definition C_Bool : Prop := forall A, A -> A -> A.
Definition c_true : C_Bool := fun A t f => t.
Definition c_false : C_Bool := fun A t f => f.

Definition T_Bool := Prop -> Prop -> Prop.
Definition t_true : T_Bool := fun t f => t.
Definition t_false : T_Bool := fun t f => f.

Definition I_Bool (t_b : T_Bool) : Prop :=
  forall P, P t_true -> P t_false -> P t_b.
Definition i_true : I_Bool t_true := fun P t f => t.
Definition i_false : I_Bool t_false := fun P t f => f.

Definition W_Bool := {t_b : T_Bool | I_Bool t_b}.
Definition w_true : W_Bool := exist _ t_true i_true.
Definition w_false : W_Bool := exist _ t_false i_false.

Definition weak_ind w_b :
  forall P : W_Bool -> Prop,
    (forall i_b, P (exist _ t_true i_b)) ->
    (forall i_b, P (exist _ t_false i_b)) -> P w_b.
  intros P t f; destruct w_b as [t_b i_b]; simpl in *.
  refine (i_b (fun t_b => forall i_b, _) _ _ i_b); auto.
Defined.

Definition Bool :=
  {w_b : W_Bool | proj1_sig w_b (w_true = w_b) (w_false = w_b)}.
Definition true : Bool := exist _ w_true eq_refl.
Definition false : Bool := exist _ w_false eq_refl.

Definition true_next_eq {w_b : W_Bool} (w : w_true = w_b) : w_true = w_b.
  induction w_b using weak_ind.
  exact (
    match w in (_ = w_b) return
      (proj1_sig w_b (w_true = w_b) (w_false = w_b))
    with
    | eq_refl => eq_refl
    end 
  ).
  exact w.
Defined.
Definition false_next_eq {w_b : W_Bool} (w : w_false = w_b) : w_false = w_b.
  induction w_b using weak_ind.
  exact w.
  exact (
    match w in (_ = w_b) return
      (proj1_sig w_b (w_true = w_b) (w_false = w_b))
    with
    | eq_refl => eq_refl
    end 
  ).
Defined.

Lemma true_eq w : true = exist _ w_true w.
  apply (sig_ext true (exist _ _ _) w).
  unfold eq_rect; simpl.
  exact (
    match w in (_ = w_b) return true_next_eq w = w with
    | eq_refl => eq_refl
    end
  ).
Defined.
Lemma false_eq w : false = exist _ w_false w.
  apply (sig_ext false (exist _ _ _) w).
  unfold eq_rect; simpl.
  exact (
    match w in (_ = w_b) return false_next_eq w = w with
    | eq_refl => eq_refl
    end
  ).
Defined.

Definition case (b : Bool) : Prop -> Prop -> Prop :=
  proj1_sig (proj1_sig b).

Definition ind (b : Bool)
  : forall P : Bool -> Prop, P true -> P false -> P b.
  intros P t f; destruct b as [w_b w]; simpl in *.
  induction w_b using weak_ind.
  refine (
    match w in (_ = w_b) return
      forall w, P (exist _ w_b w) with
    | eq_refl => _
    end w
  ); clear w; intros w.
  rewrite <- (true_eq w); exact t.
  refine (
    match w in (_ = w_b) return
      forall w, P (exist _ w_b w) with
    | eq_refl => _
    end w
  ); clear w; intros w.
  rewrite <- (false_eq w); exact f.
Defined.