what_does_inversion_do_with_false~=true.v

Definition true_not_false : true = false ->False :=
  fun H =>
    match H (*in _ = b
            return if b then True else False*)
    with
    | eq_refl => I:True
    end.