proposition: Lemma FIdE (A B : UU0) (f : A -> B) : idfun # f = f.
proof: Proof. by []. Qed.
imports: ssrmatching Reals JMeq mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra Rstruct reals) infotheo(Reals_ext) infotheo(realType_ext) monae_lib HB(structures)