DEFINITION subst0_refl()
TYPE =
       ∀u:T.∀t:T.∀d:nat.(subst0 d u t t)→∀P:Prop.P
BODY =
Show proof