proposition: Lemma extends_order : forall A B (E:binary B), equiv E -> order_wrt (partial_equiv E) (@extends A B E).
proof: Proof. Proof using. unfold extends. constructor. intros_all. dauto. introv [D1 H1] [D2 H2]. unfolds pfun_equiv. dauto. introv [D1 H1] [D2 H2]. split. extens*. dauto. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)