fact: Definition Let_In_pf {A P} (x : A) (f : forall a : A, a = x -> P a) : P x := let y := x in f y eq_refl.
imports: Coq.Classes.Morphisms Coq.Relations.Relation_Definitions Fiat.Common.Tactics.GetGoal Fiat.Common.Notations