Using bool_ind

Give two proofs of the following theorem :
bool_equal : (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

boolequal.v


Going home
Pierre Castéran