Let J and le be given.

Assume HJ: directed_set J le.

An exact proof term for the current goal is (partial_order_on_refl J le (directed_set_partial_order J le HJ)).

∎