Thetheorem%\index{Gallinaterms!UIP\_refl}%[UIP_refl]comesfromthe[Eqdep]moduleofthestandardlibrary.(Itsnameusestheacronym"UIP"for"unicity of identity proofs.")DotheCoqauthorsknowofsomeclevertrickforbuildingsuchproofsthatwehavenotseenyet?Iftheydo,theydidnotuseitforthisproof.Rather,theproofisbasedonan_axiom_,theterm[eq_rect_eq]below.*)
@@ -691,7 +690,7 @@ Inductive JMeq (A : Type) (x : A) : forall B : Type, B -> Prop :=
JMeq_refl:JMeqxx
]]
Theidentifier[JMeq]standsfor%\index{JohnMajorequality}%"John Major equality,"anamecoinedbyConorMcBride%~\cite{JMeq}%asasortofpunaboutBritishpolitics.Thedefinition[JMeq]startsoutlookingalotlikethedefinitionof[eq].Thecrucialdifferenceisthatwemayuse[JMeq]_onargumentsofdifferenttypes_.Forinstance,alemmathatwefailedtoestablishbeforeistrivialwith[JMeq].Itmakesforprettiertheoremstatementstodefinesomesyntacticshorthandfirst.*)
Theidentifier[JMeq]standsfor%\index{JohnMajorequality}%"John Major equality,"anamecoinedbyConorMcBride%~\cite{JMeq}%asaninsidejokeaboutBritishpolitics.Thedefinition[JMeq]startsoutlookingalotlikethedefinitionof[eq].Thecrucialdifferenceisthatwemayuse[JMeq]_onargumentsofdifferenttypes_.Forinstance,alemmathatwefailedtoestablishbeforeistrivialwith[JMeq].Itmakesforprettiertheoremstatementstodefinesomesyntacticshorthandfirst.*)