proposition: Lemma UIP_refl_nat (n:nat) (x : n = n) : x = eq_refl.
proof: Proof. induction n as [|n IHn]. - change (match 0 as n return 0=n -> Prop with | 0 => fun x => x = eq_refl | _ => fun _ => True end x). destruct x; reflexivity. - specialize IHn with (f_equal pred x). change eq_refl with (f_equal S (@eq_refl _ n)). rewrite <- IHn; clear IHn. change (match S n as n' return S n = n' -> Prop with | 0 => fun _ => True | S n' => fun x => x = f_equal S (f_equal pred x) end x). pattern (S n) at 2 3, x. destruct x; reflexivity. Defined.