fact: Definition cate_moveR_eM {A} `{HasEquivs A} {a b c : A} (e : b $<~> a) (f : b $<~> c) (g : a $<~> c) (p : cate_fun g $== f $o e^-1$) : g $o e $== f.
imports: Basics.Utf8 Basics.Overture Basics.Tactics WildCat.Core