Using bool_ind

Give two proofs of the following theorem : 
bool_cases : (b:bool)b=true\/b=false
  1. Give directly a proof term, with occurences of bool_ind, or_introl, or_intror and refl_equal.
  2. Use the following tactics : pattern, apply, left, right, and reflexivity.

Solution

bool_cases.v