proposition: Lemma UIP_refl_bool (b:bool) (x : b = b) : x = eq_refl.
proof: Proof. destruct b. - change (match true as b return true=b -> Prop with | true => fun x => x = eq_refl | _ => fun _ => True end x). destruct x; reflexivity. - change (match false as b return false=b -> Prop with | false => fun x => x = eq_refl | _ => fun _ => True end x). destruct x; reflexivity. Defined.