proposition: Lemma partial_equiv_equiv : forall A B (E:binary B), equiv E -> equiv (@partial_equiv A B E).
proof: Proof. Proof using. introv Equi. unfold partial_equiv. constructor. intros_all. dauto. introv [D H]. rewrite D in *. dauto. introv [D1 H1] [D2 H2]. rewrite D1,D2 in *. dauto. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)