Let J and le be given.
We will
prove ∀a : set, a ∈ J → (a,a) ∈ le.
Let a be given.
We prove the intermediate
claim Htmp:
(relation_on le J ∧ (∀a0 : set, a0 ∈ J → (a0,a0) ∈ le)) ∧ (∀a0 b0 : set, a0 ∈ J → b0 ∈ J → (a0,b0) ∈ le → (b0,a0) ∈ le → a0 = b0).
An
exact proof term for the current goal is
(andEL ((relation_on le J ∧ (∀a0 : set, a0 ∈ J → (a0,a0) ∈ le)) ∧ (∀a0 b0 : set, a0 ∈ J → b0 ∈ J → (a0,b0) ∈ le → (b0,a0) ∈ le → a0 = b0)) (∀a0 b0 c0 : set, a0 ∈ J → b0 ∈ J → c0 ∈ J → (a0,b0) ∈ le → (b0,c0) ∈ le → (a0,c0) ∈ le) Hpo).
We prove the intermediate
claim Hrelrefl:
relation_on le J ∧ (∀a0 : set, a0 ∈ J → (a0,a0) ∈ le).
An
exact proof term for the current goal is
(andEL (relation_on le J ∧ (∀a0 : set, a0 ∈ J → (a0,a0) ∈ le)) (∀a0 b0 : set, a0 ∈ J → b0 ∈ J → (a0,b0) ∈ le → (b0,a0) ∈ le → a0 = b0) Htmp).
We prove the intermediate
claim Hrefl:
∀a0 : set, a0 ∈ J → (a0,a0) ∈ le.
An
exact proof term for the current goal is
(andER (relation_on le J) (∀a0 : set, a0 ∈ J → (a0,a0) ∈ le) Hrelrefl).
An exact proof term for the current goal is (Hrefl a HaJ).
∎