r=r' → r⎻* = r'⎻*.
#P; #Q; #a; #a'; #e; #x; #x'; #Hx; napply (.= †Hx);
napply oa_leq_antisym; napply ORelation_eq_respects_leq_or_f_minus_star_
r=r' → r⎻* = r'⎻*.
#P; #Q; #a; #a'; #e; #x; #x'; #Hx; napply (.= †Hx);
napply oa_leq_antisym; napply ORelation_eq_respects_leq_or_f_minus_star_