fact: Definition Eps : F \O G ~> FId := (eps1) \v [NEq F1 \O FId \O G1 , F1 \O G1] \v (NId F1 \h eps0 \h NId G1) \v [NEq F \O G , (F1 \O (F0 \O G0)) \O G1].
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib HB(structures)