Fixpoint a (_:unit):=
match eq_refl with
|eq_refl => a
end.