Let x and y be given.
Assume Hx Hy.
Let p be given.
Assume Hp.
We will prove p.
Set Lxy1 to be the term {(w 0) * y + x * (w 1) + - (w 0) * (w 1)|w ∈ SNoL x ⨯ SNoL y}.
Set Lxy2 to be the term {(z 0) * y + x * (z 1) + - (z 0) * (z 1)|z ∈ SNoR x ⨯ SNoR y}.
Set Rxy1 to be the term {(w 0) * y + x * (w 1) + - (w 0) * (w 1)|w ∈ SNoL x ⨯ SNoR y}.
Set Rxy2 to be the term {(z 0) * y + x * (z 1) + - (z 0) * (z 1)|z ∈ SNoR x ⨯ SNoL y}.
Apply Hp (Lxy1 ∪ Lxy2) (Rxy1 ∪ Rxy2) to the current goal.
Let u be given.
Assume Hu.
Let q be given.
Assume Hq1: ∀w0 ∈ SNoL x, ∀w1 ∈ SNoL y, u = w0 * y + x * w1 + - w0 * w1 → q.
Assume Hq2: ∀z0 ∈ SNoR x, ∀z1 ∈ SNoR y, u = z0 * y + x * z1 + - z0 * z1 → q.
Apply binunionE Lxy1 Lxy2 u Hu to the current goal.
Assume Hu1: u ∈ Lxy1.
Apply ReplE_impred (SNoL x ⨯ SNoL y) (λw ⇒ (w 0) * y + x * (w 1) + - (w 0) * (w 1)) u Hu1 to the current goal.
Let w be given.
Assume Hw: w ∈ SNoL x ⨯ SNoL y.
Assume Hw2: u = (w 0) * y + x * (w 1) + - (w 0) * (w 1).
An exact proof term for the current goal is Hq1 (w 0) (ap0_Sigma (SNoL x) (λ_ ⇒ SNoL y) w Hw) (w 1) (ap1_Sigma (SNoL x) (λ_ ⇒ SNoL y) w Hw) Hw2.
Assume Hu2: u ∈ Lxy2.
Apply ReplE_impred (SNoR x ⨯ SNoR y) (λz ⇒ (z 0) * y + x * (z 1) + - (z 0) * (z 1)) u Hu2 to the current goal.
Let z be given.
Assume Hz: z ∈ SNoR x ⨯ SNoR y.
Assume Hz2: u = (z 0) * y + x * (z 1) + - (z 0) * (z 1).
An exact proof term for the current goal is Hq2 (z 0) (ap0_Sigma (SNoR x) (λ_ ⇒ SNoR y) z Hz) (z 1) (ap1_Sigma (SNoR x) (λ_ ⇒ SNoR y) z Hz) Hz2.
Let w0 be given.
Assume Hw0: w0 ∈ SNoL x.
Let w1 be given.
Assume Hw1: w1 ∈ SNoL y.
We will prove w0 * y + x * w1 + - w0 * w1 ∈ Lxy1 ∪ Lxy2.
Apply binunionI1 to the current goal.
We will prove w0 * y + x * w1 + - w0 * w1 ∈ Lxy1.
Apply tuple_2_0_eq w0 w1 (λu v ⇒ u * y + x * w1 + - u * w1 ∈ Lxy1) to the current goal.
We will prove (w0,w1) 0 * y + x * w1 + - (w0,w1) 0 * w1 ∈ Lxy1.
Apply tuple_2_1_eq w0 w1 (λu v ⇒ (w0,w1) 0 * y + x * u + - (w0,w1) 0 * u ∈ Lxy1) to the current goal.
We will prove (w0,w1) 0 * y + x * (w0,w1) 1 + - (w0,w1) 0 * (w0,w1) 1 ∈ Lxy1.
Apply ReplI (SNoL x ⨯ SNoL y) (λw ⇒ (w 0) * y + x * (w 1) + - (w 0) * (w 1)) (w0,w1) to the current goal.
We will prove (w0,w1) ∈ SNoL x ⨯ SNoL y.
Apply tuple_2_setprod to the current goal.
An exact proof term for the current goal is Hw0.
An exact proof term for the current goal is Hw1.
Let z0 be given.
Assume Hz0: z0 ∈ SNoR x.
Let z1 be given.
Assume Hz1: z1 ∈ SNoR y.
We will prove z0 * y + x * z1 + - z0 * z1 ∈ Lxy1 ∪ Lxy2.
Apply binunionI2 to the current goal.
We will prove z0 * y + x * z1 + - z0 * z1 ∈ Lxy2.
Apply tuple_2_0_eq z0 z1 (λu v ⇒ u * y + x * z1 + - u * z1 ∈ Lxy2) to the current goal.
We will prove (z0,z1) 0 * y + x * z1 + - (z0,z1) 0 * z1 ∈ Lxy2.
Apply tuple_2_1_eq z0 z1 (λu v ⇒ (z0,z1) 0 * y + x * u + - (z0,z1) 0 * u ∈ Lxy2) to the current goal.
We will prove (z0,z1) 0 * y + x * (z0,z1) 1 + - (z0,z1) 0 * (z0,z1) 1 ∈ Lxy2.
Apply ReplI (SNoR x ⨯ SNoR y) (λz ⇒ (z 0) * y + x * (z 1) + - (z 0) * (z 1)) (z0,z1) to the current goal.
We will prove (z0,z1) ∈ SNoR x ⨯ SNoR y.
Apply tuple_2_setprod to the current goal.
An exact proof term for the current goal is Hz0.
An exact proof term for the current goal is Hz1.
Let u be given.
Assume Hu.
Let q be given.
Assume Hq1 Hq2.
Apply binunionE Rxy1 Rxy2 u Hu to the current goal.
Assume Hu1: u ∈ Rxy1.
Apply ReplE_impred (SNoL x ⨯ SNoR y) (λw ⇒ (w 0) * y + x * (w 1) + - (w 0) * (w 1)) u Hu1 to the current goal.
Let w be given.
Assume Hw: w ∈ SNoL x ⨯ SNoR y.
Assume Hw2: u = (w 0) * y + x * (w 1) + - (w 0) * (w 1).
An exact proof term for the current goal is Hq1 (w 0) (ap0_Sigma (SNoL x) (λ_ ⇒ SNoR y) w Hw) (w 1) (ap1_Sigma (SNoL x) (λ_ ⇒ SNoR y) w Hw) Hw2.
Assume Hu2: u ∈ Rxy2.
Apply ReplE_impred (SNoR x ⨯ SNoL y) (λz ⇒ (z 0) * y + x * (z 1) + - (z 0) * (z 1)) u Hu2 to the current goal.
Let z be given.
Assume Hz: z ∈ SNoR x ⨯ SNoL y.
Assume Hz2: u = (z 0) * y + x * (z 1) + - (z 0) * (z 1).
An exact proof term for the current goal is Hq2 (z 0) (ap0_Sigma (SNoR x) (λ_ ⇒ SNoL y) z Hz) (z 1) (ap1_Sigma (SNoR x) (λ_ ⇒ SNoL y) z Hz) Hz2.
Let w0 be given.
Assume Hw0: w0 ∈ SNoL x.
Let z1 be given.
Assume Hz1: z1 ∈ SNoR y.
We will prove w0 * y + x * z1 + - w0 * z1 ∈ Rxy1 ∪ Rxy2.
Apply binunionI1 to the current goal.
We will prove w0 * y + x * z1 + - w0 * z1 ∈ Rxy1.
Apply tuple_2_0_eq w0 z1 (λu v ⇒ u * y + x * z1 + - u * z1 ∈ Rxy1) to the current goal.
We will prove (w0,z1) 0 * y + x * z1 + - (w0,z1) 0 * z1 ∈ Rxy1.
Apply tuple_2_1_eq w0 z1 (λu v ⇒ (w0,z1) 0 * y + x * u + - (w0,z1) 0 * u ∈ Rxy1) to the current goal.
We will prove (w0,z1) 0 * y + x * (w0,z1) 1 + - (w0,z1) 0 * (w0,z1) 1 ∈ Rxy1.
Apply ReplI (SNoL x ⨯ SNoR y) (λw ⇒ (w 0) * y + x * (w 1) + - (w 0) * (w 1)) (w0,z1) to the current goal.
We will prove (w0,z1) ∈ SNoL x ⨯ SNoR y.
Apply tuple_2_setprod to the current goal.
An exact proof term for the current goal is Hw0.
An exact proof term for the current goal is Hz1.
Let z0 be given.
Assume Hz0: z0 ∈ SNoR x.
Let w1 be given.
Assume Hw1: w1 ∈ SNoL y.
We will prove z0 * y + x * w1 + - z0 * w1 ∈ Rxy1 ∪ Rxy2.
Apply binunionI2 to the current goal.
We will prove z0 * y + x * w1 + - z0 * w1 ∈ Rxy2.
Apply tuple_2_0_eq z0 w1 (λu v ⇒ u * y + x * w1 + - u * w1 ∈ Rxy2) to the current goal.
We will prove (z0,w1) 0 * y + x * w1 + - (z0,w1) 0 * w1 ∈ Rxy2.
Apply tuple_2_1_eq z0 w1 (λu v ⇒ (z0,w1) 0 * y + x * u + - (z0,w1) 0 * u ∈ Rxy2) to the current goal.
We will prove (z0,w1) 0 * y + x * (z0,w1) 1 + - (z0,w1) 0 * (z0,w1) 1 ∈ Rxy2.
Apply ReplI (SNoR x ⨯ SNoL y) (λw ⇒ (w 0) * y + x * (w 1) + - (w 0) * (w 1)) (z0,w1) to the current goal.
We will prove (z0,w1) ∈ SNoR x ⨯ SNoL y.
Apply tuple_2_setprod to the current goal.
An exact proof term for the current goal is Hz0.
An exact proof term for the current goal is Hw1.
An exact proof term for the current goal is mul_SNo_eq x Hx y Hy.
∎