casebool.v

Inductive bool : Type := |true | false.

Inductive eq A x : A -> Prop := eq_refl : eq A x x.

Inductive or A B : Prop:=
   | or_introl : A -> or A B
   | or_intror : B -> or A B.

Definition case_bool x : or (eq bool x true) (eq bool x false) :=
   match x with
      | true => or_introl (eq bool true true) (eq bool true false) (eq_refl bool true)
      | false=> or_intror (eq bool false true) (eq bool false false) (eq_refl bool false)
   end.

Print case_bool.
Check case_bool.
Check (forall x : bool, or (eq bool x true) (eq bool x false)).

Check (or (eq bool true true) (eq bool true false)).

Check (fun x:bool => true).
Check (bool -> bool).

(*  https://coq.inria.fr/refman/Reference-Manual003.html#caseanalysis *)