Assume HX2o.
We prove the intermediate
claim Hex:
∃i m j n : set, (i ∈ 2 ∧ m ∈ ω ∧ j ∈ 2 ∧ n ∈ ω ∧ x = (i,m) ∧ x = (j,n) ∧ (i ∈ j ∨ (i = j ∧ m ∈ n))).
Apply Hex to the current goal.
Let i be given.
Assume Hmjn.
Apply Hmjn to the current goal.
Let m be given.
Assume Hjnn.
Apply Hjnn to the current goal.
Let j be given.
Assume Hnn.
Apply Hnn to the current goal.
Let n be given.
Assume Hpack.
We prove the intermediate
claim Hcoords5:
(i ∈ 2 ∧ m ∈ ω ∧ j ∈ 2 ∧ n ∈ ω ∧ x = (i,m) ∧ x = (j,n)).
An
exact proof term for the current goal is
(andEL (i ∈ 2 ∧ m ∈ ω ∧ j ∈ 2 ∧ n ∈ ω ∧ x = (i,m) ∧ x = (j,n)) (i ∈ j ∨ (i = j ∧ m ∈ n)) Hpack).
We prove the intermediate
claim Hcmp:
i ∈ j ∨ (i = j ∧ m ∈ n).
An
exact proof term for the current goal is
(andER (i ∈ 2 ∧ m ∈ ω ∧ j ∈ 2 ∧ n ∈ ω ∧ x = (i,m) ∧ x = (j,n)) (i ∈ j ∨ (i = j ∧ m ∈ n)) Hpack).
We prove the intermediate
claim Hcoords4:
(i ∈ 2 ∧ m ∈ ω ∧ j ∈ 2 ∧ n ∈ ω ∧ x = (i,m)).
An
exact proof term for the current goal is
(andEL (i ∈ 2 ∧ m ∈ ω ∧ j ∈ 2 ∧ n ∈ ω ∧ x = (i,m)) (x = (j,n)) Hcoords5).
We prove the intermediate
claim Hxjn:
x = (j,n).
An
exact proof term for the current goal is
(andER (i ∈ 2 ∧ m ∈ ω ∧ j ∈ 2 ∧ n ∈ ω ∧ x = (i,m)) (x = (j,n)) Hcoords5).
We prove the intermediate
claim Hxim:
x = (i,m).
An
exact proof term for the current goal is
(andER (i ∈ 2 ∧ m ∈ ω ∧ j ∈ 2 ∧ n ∈ ω) (x = (i,m)) Hcoords4).
We prove the intermediate
claim HeqPair:
(i,m) = (j,n).
rewrite the current goal using Hxim (from right to left) at position 1.
An exact proof term for the current goal is Hxjn.
We prove the intermediate
claim Hij:
i = j.
rewrite the current goal using
(tuple_2_0_eq i m) (from right to left).
rewrite the current goal using
(tuple_2_0_eq j n) (from right to left).
rewrite the current goal using HeqPair (from right to left).
Use reflexivity.
We prove the intermediate
claim Hmn:
m = n.
rewrite the current goal using
(tuple_2_1_eq i m) (from right to left).
rewrite the current goal using
(tuple_2_1_eq j n) (from right to left).
rewrite the current goal using HeqPair (from right to left).
Use reflexivity.
Apply (Hcmp False) to the current goal.
We prove the intermediate
claim Hii:
i ∈ i.
rewrite the current goal using Hij (from left to right) at position 2.
An exact proof term for the current goal is Hilj.
An
exact proof term for the current goal is
(In_irref i Hii).
We prove the intermediate
claim Hmnin:
m ∈ n.
An
exact proof term for the current goal is
(andER (i = j) (m ∈ n) Hind).
We prove the intermediate
claim Hmm:
m ∈ m.
rewrite the current goal using Hmn (from left to right) at position 2.
An exact proof term for the current goal is Hmnin.
An
exact proof term for the current goal is
(In_irref m Hmm).