Theorem ile_refl

Proof
ile_refl. ⊢ a ∈ ℤ → a ≤ a,
  pred_restr int_incl_in_real rle_refl.

Dependencies
The given proof depends on four axioms:
comp, eq_refl, eq_subst, rle_refl.