We prove the intermediate
claim H2R:
2 ∈ R.
An
exact proof term for the current goal is
(SepE1 R (λx0 : set ⇒ ¬ (Rlt x0 0) ∧ ¬ (Rlt 1 x0)) 2 H2I).
We prove the intermediate
claim Hprop:
¬ (Rlt 1 2).
We prove the intermediate
claim Hconj:
¬ (Rlt 2 0) ∧ ¬ (Rlt 1 2).
An
exact proof term for the current goal is
(SepE2 R (λx0 : set ⇒ ¬ (Rlt x0 0) ∧ ¬ (Rlt 1 x0)) 2 H2I).
An
exact proof term for the current goal is
(andER (¬ (Rlt 2 0)) (¬ (Rlt 1 2)) Hconj).
We prove the intermediate
claim H12:
Rlt 1 2.
An exact proof term for the current goal is (Hprop H12).
∎