Apply SNoLev_ind2 to the current goal.
Let x and y be given.
Assume Hx Hy.
Assume IHx: ∀w ∈ SNoS_ (SNoLev x), (- w) * y = - w * y.
Assume IHy: ∀z ∈ SNoS_ (SNoLev y), (- x) * z = - x * z.
Assume IHxy: ∀w ∈ SNoS_ (SNoLev x), ∀z ∈ SNoS_ (SNoLev y), (- w) * z = - w * z.
We prove the intermediate claim Lmx: SNo (- x).
An exact proof term for the current goal is SNo_minus_SNo x Hx.
Apply mul_SNo_eq_3 x y Hx Hy to the current goal.
Let L and R be given.
Assume HLR HLE HLI1 HLI2 HRE HRI1 HRI2.
Assume Hxye: x * y = SNoCut L R.
Apply mul_SNo_eq_3 (- x) y (SNo_minus_SNo x Hx) Hy to the current goal.
Let L' and R' be given.
Assume HL'R' HL'E HL'I1 HL'I2 HR'E HR'I1 HR'I2.
Assume Hmxye: (- x) * y = SNoCut L' R'.
We prove the intermediate claim L1: - (x * y) = SNoCut {- z|z ∈ R} {- w|w ∈ L}.
rewrite the current goal using Hxye (from left to right).
An exact proof term for the current goal is minus_SNoCut_eq L R HLR.
rewrite the current goal using L1 (from left to right).
rewrite the current goal using Hmxye (from left to right).
We will prove SNoCut L' R' = SNoCut {- z|z ∈ R} {- w|w ∈ L}.
Use f_equal.
We will prove L' = {- z|z ∈ R}.
Apply set_ext to the current goal.
Apply mul_SNo_Subq_lem (- x) y (SNoL (- x)) (SNoL y) (SNoR (- x)) (SNoR y) L' {- z|z ∈ R} HL'E to the current goal.
Let u be given.
Assume Hu: u ∈ SNoL (- x).
Let v be given.
Assume Hv: v ∈ SNoL y.
Apply SNoL_E (- x) Lmx u Hu to the current goal.
Assume Hua: SNo u.
Assume Hub: SNoLev u ∈ SNoLev (- x).
Assume Huc: u < - x.
Apply SNoL_E y Hy v Hv to the current goal.
Assume Hva _ _.
We prove the intermediate claim Lmu1: SNo (- u).
An exact proof term for the current goal is SNo_minus_SNo u Hua.
We prove the intermediate claim Lmu2: - u ∈ SNoR x.
Apply SNoR_I x Hx (- u) Lmu1 to the current goal.
We will prove SNoLev (- u) ∈ SNoLev x.
rewrite the current goal using minus_SNo_Lev u Hua (from left to right).
rewrite the current goal using minus_SNo_Lev x Hx (from right to left).
An exact proof term for the current goal is Hub.
We will prove x < - u.
An exact proof term for the current goal is minus_SNo_Lt_contra2 u x Hua Hx Huc.
We will prove u * y + (- x) * v + - u * v ∈ {- z|z ∈ R}.
We prove the intermediate claim L1: u * y + (- x) * v + - u * v = - ((- u) * y + x * v + - (- u) * v).
Use symmetry.
Use transitivity with and - (- u) * y + - x * v + - - (- u) * v.
An exact proof term for the current goal is minus_add_SNo_distr_3 ((- u) * y) (x * v) (- (- u) * v) (SNo_mul_SNo (- u) y Lmu1 Hy) (SNo_mul_SNo x v Hx Hva) (SNo_minus_SNo ((- u) * v) (SNo_mul_SNo (- u) v Lmu1 Hva)).
Use f_equal.
We will prove - (- u) * y = u * y.
Use transitivity with and (- - u) * y.
Use symmetry.
An exact proof term for the current goal is IHx (- u) (SNoR_SNoS x Hx (- u) Lmu2).
rewrite the current goal using minus_SNo_invol u Hua (from left to right).
Use reflexivity.
Use f_equal.
We will prove - x * v = (- x) * v.
Use symmetry.
An exact proof term for the current goal is IHy v (SNoL_SNoS y Hy v Hv).
Use f_equal.
We will prove - (- u) * v = u * v.
Use transitivity with and (- - u) * v.
Use symmetry.
We will prove (- - u) * v = - (- u) * v.
An exact proof term for the current goal is IHxy (- u) (SNoR_SNoS x Hx (- u) Lmu2) v (SNoL_SNoS y Hy v Hv).
rewrite the current goal using minus_SNo_invol u Hua (from left to right).
Use reflexivity.
rewrite the current goal using L1 (from left to right).
We will prove - ((- u) * y + x * v + - (- u) * v) ∈ {- z|z ∈ R}.
Apply ReplI R (λz ⇒ - z) to the current goal.
We will prove (- u) * y + x * v + - (- u) * v ∈ R.
Apply HRI2 to the current goal.
We will prove - u ∈ SNoR x.
An exact proof term for the current goal is Lmu2.
We will prove v ∈ SNoL y.
An exact proof term for the current goal is Hv.
Let u be given.
Assume Hu: u ∈ SNoR (- x).
Let v be given.
Assume Hv: v ∈ SNoR y.
Apply SNoR_E (- x) Lmx u Hu to the current goal.
Assume Hua: SNo u.
Assume Hub: SNoLev u ∈ SNoLev (- x).
Assume Huc: - x < u.
Apply SNoR_E y Hy v Hv to the current goal.
Assume Hva _ _.
We prove the intermediate claim Lmu1: SNo (- u).
An exact proof term for the current goal is SNo_minus_SNo u Hua.
We prove the intermediate claim Lmu2: - u ∈ SNoL x.
Apply SNoL_I x Hx (- u) Lmu1 to the current goal.
We will prove SNoLev (- u) ∈ SNoLev x.
rewrite the current goal using minus_SNo_Lev u Hua (from left to right).
rewrite the current goal using minus_SNo_Lev x Hx (from right to left).
An exact proof term for the current goal is Hub.
We will prove - u < x.
An exact proof term for the current goal is minus_SNo_Lt_contra1 x u Hx Hua Huc.
We will prove u * y + (- x) * v + - u * v ∈ {- z|z ∈ R}.
We prove the intermediate claim L1: u * y + (- x) * v + - u * v = - ((- u) * y + x * v + - (- u) * v).
Use symmetry.
Use transitivity with and - (- u) * y + - x * v + - - (- u) * v.
An exact proof term for the current goal is minus_add_SNo_distr_3 ((- u) * y) (x * v) (- (- u) * v) (SNo_mul_SNo (- u) y Lmu1 Hy) (SNo_mul_SNo x v Hx Hva) (SNo_minus_SNo ((- u) * v) (SNo_mul_SNo (- u) v Lmu1 Hva)).
Use f_equal.
We will prove - (- u) * y = u * y.
Use transitivity with and (- - u) * y.
Use symmetry.
An exact proof term for the current goal is IHx (- u) (SNoL_SNoS x Hx (- u) Lmu2).
rewrite the current goal using minus_SNo_invol u Hua (from left to right).
Use reflexivity.
Use f_equal.
We will prove - x * v = (- x) * v.
Use symmetry.
An exact proof term for the current goal is IHy v (SNoR_SNoS y Hy v Hv).
Use f_equal.
We will prove - (- u) * v = u * v.
Use transitivity with and (- - u) * v.
Use symmetry.
We will prove (- - u) * v = - (- u) * v.
An exact proof term for the current goal is IHxy (- u) (SNoL_SNoS x Hx (- u) Lmu2) v (SNoR_SNoS y Hy v Hv).
rewrite the current goal using minus_SNo_invol u Hua (from left to right).
Use reflexivity.
rewrite the current goal using L1 (from left to right).
We will prove - ((- u) * y + x * v + - (- u) * v) ∈ {- z|z ∈ R}.
Apply ReplI R (λz ⇒ - z) to the current goal.
We will prove (- u) * y + x * v + - (- u) * v ∈ R.
Apply HRI1 to the current goal.
We will prove - u ∈ SNoL x.
An exact proof term for the current goal is Lmu2.
We will prove v ∈ SNoR y.
An exact proof term for the current goal is Hv.
We will prove {- z|z ∈ R} ⊆ L'.
Let a be given.
Assume Ha.
Apply ReplE_impred R (λz ⇒ - z) a Ha to the current goal.
Let z be given.
Assume Hz: z ∈ R.
Assume Hze: a = - z.
rewrite the current goal using Hze (from left to right).
We will prove - z ∈ L'.
Apply HRE z Hz to the current goal.
Let u be given.
Assume Hu: u ∈ SNoL x.
Let v be given.
Assume Hv: v ∈ SNoR y.
Assume Hzuv: z = u * y + x * v + - u * v.
Apply SNoL_E x Hx u Hu to the current goal.
Assume Hua: SNo u.
Assume Hub: SNoLev u ∈ SNoLev x.
Assume Huc: u < x.
Apply SNoR_E y Hy v Hv to the current goal.
Assume Hva _ _.
We prove the intermediate claim Lmu1: SNo (- u).
An exact proof term for the current goal is SNo_minus_SNo u Hua.
We prove the intermediate claim Lmu2: - u ∈ SNoR (- x).
Apply SNoR_I (- x) (SNo_minus_SNo x Hx) (- u) Lmu1 to the current goal.
We will prove SNoLev (- u) ∈ SNoLev (- x).
rewrite the current goal using minus_SNo_Lev u Hua (from left to right).
rewrite the current goal using minus_SNo_Lev x Hx (from left to right).
An exact proof term for the current goal is Hub.
We will prove - x < - u.
An exact proof term for the current goal is minus_SNo_Lt_contra u x Hua Hx Huc.
We prove the intermediate claim L1: - z = (- u) * y + (- x) * v + - (- u) * v.
rewrite the current goal using Hzuv (from left to right).
rewrite the current goal using minus_add_SNo_distr_3 (u * y) (x * v) (- (u * v)) (SNo_mul_SNo u y Hua Hy) (SNo_mul_SNo x v Hx Hva) (SNo_minus_SNo (u * v) (SNo_mul_SNo u v Hua Hva)) (from left to right).
Use f_equal.
We will prove - (u * y) = (- u) * y.
Use symmetry.
An exact proof term for the current goal is IHx u (SNoL_SNoS x Hx u Hu).
Use f_equal.
We will prove - (x * v) = (- x) * v.
Use symmetry.
An exact proof term for the current goal is IHy v (SNoR_SNoS y Hy v Hv).
Use f_equal.
We will prove - (u * v) = (- u) * v.
Use symmetry.
An exact proof term for the current goal is IHxy u (SNoL_SNoS x Hx u Hu) v (SNoR_SNoS y Hy v Hv).
rewrite the current goal using L1 (from left to right).
We will prove (- u) * y + (- x) * v + - (- u) * v ∈ L'.
Apply HL'I2 to the current goal.
An exact proof term for the current goal is Lmu2.
An exact proof term for the current goal is Hv.
Let u be given.
Assume Hu: u ∈ SNoR x.
Let v be given.
Assume Hv: v ∈ SNoL y.
Assume Hzuv: z = u * y + x * v + - u * v.
Apply SNoR_E x Hx u Hu to the current goal.
Assume Hua: SNo u.
Assume Hub: SNoLev u ∈ SNoLev x.
Assume Huc: x < u.
Apply SNoL_E y Hy v Hv to the current goal.
Assume Hva _ _.
We prove the intermediate claim Lmu1: SNo (- u).
An exact proof term for the current goal is SNo_minus_SNo u Hua.
We prove the intermediate claim Lmu2: - u ∈ SNoL (- x).
Apply SNoL_I (- x) (SNo_minus_SNo x Hx) (- u) Lmu1 to the current goal.
We will prove SNoLev (- u) ∈ SNoLev (- x).
rewrite the current goal using minus_SNo_Lev u Hua (from left to right).
rewrite the current goal using minus_SNo_Lev x Hx (from left to right).
An exact proof term for the current goal is Hub.
We will prove - u < - x.
An exact proof term for the current goal is minus_SNo_Lt_contra x u Hx Hua Huc.
We prove the intermediate claim L1: - z = (- u) * y + (- x) * v + - (- u) * v.
rewrite the current goal using Hzuv (from left to right).
rewrite the current goal using minus_add_SNo_distr_3 (u * y) (x * v) (- (u * v)) (SNo_mul_SNo u y Hua Hy) (SNo_mul_SNo x v Hx Hva) (SNo_minus_SNo (u * v) (SNo_mul_SNo u v Hua Hva)) (from left to right).
Use f_equal.
We will prove - (u * y) = (- u) * y.
Use symmetry.
An exact proof term for the current goal is IHx u (SNoR_SNoS x Hx u Hu).
Use f_equal.
We will prove - (x * v) = (- x) * v.
Use symmetry.
An exact proof term for the current goal is IHy v (SNoL_SNoS y Hy v Hv).
Use f_equal.
We will prove - (u * v) = (- u) * v.
Use symmetry.
An exact proof term for the current goal is IHxy u (SNoR_SNoS x Hx u Hu) v (SNoL_SNoS y Hy v Hv).
rewrite the current goal using L1 (from left to right).
We will prove (- u) * y + (- x) * v + - (- u) * v ∈ L'.
Apply HL'I1 to the current goal.
An exact proof term for the current goal is Lmu2.
An exact proof term for the current goal is Hv.
We will prove R' = {- w|w ∈ L}.
Apply set_ext to the current goal.
Apply mul_SNo_Subq_lem (- x) y (SNoL (- x)) (SNoR y) (SNoR (- x)) (SNoL y) R' {- w|w ∈ L} HR'E to the current goal.
Let u be given.
Assume Hu: u ∈ SNoL (- x).
Let v be given.
Assume Hv: v ∈ SNoR y.
Apply SNoL_E (- x) Lmx u Hu to the current goal.
Assume Hua: SNo u.
Assume Hub: SNoLev u ∈ SNoLev (- x).
Assume Huc: u < - x.
Apply SNoR_E y Hy v Hv to the current goal.
Assume Hva _ _.
We prove the intermediate claim Lmu1: SNo (- u).
An exact proof term for the current goal is SNo_minus_SNo u Hua.
We prove the intermediate claim Lmu2: - u ∈ SNoR x.
Apply SNoR_I x Hx (- u) Lmu1 to the current goal.
We will prove SNoLev (- u) ∈ SNoLev x.
rewrite the current goal using minus_SNo_Lev u Hua (from left to right).
rewrite the current goal using minus_SNo_Lev x Hx (from right to left).
An exact proof term for the current goal is Hub.
We will prove x < - u.
An exact proof term for the current goal is minus_SNo_Lt_contra2 u x Hua Hx Huc.
We will prove u * y + (- x) * v + - u * v ∈ {- w|w ∈ L}.
We prove the intermediate claim L1: u * y + (- x) * v + - u * v = - ((- u) * y + x * v + - (- u) * v).
Use symmetry.
Use transitivity with and - (- u) * y + - x * v + - - (- u) * v.
An exact proof term for the current goal is minus_add_SNo_distr_3 ((- u) * y) (x * v) (- (- u) * v) (SNo_mul_SNo (- u) y Lmu1 Hy) (SNo_mul_SNo x v Hx Hva) (SNo_minus_SNo ((- u) * v) (SNo_mul_SNo (- u) v Lmu1 Hva)).
Use f_equal.
We will prove - (- u) * y = u * y.
Use transitivity with and (- - u) * y.
Use symmetry.
An exact proof term for the current goal is IHx (- u) (SNoR_SNoS x Hx (- u) Lmu2).
rewrite the current goal using minus_SNo_invol u Hua (from left to right).
Use reflexivity.
Use f_equal.
We will prove - x * v = (- x) * v.
Use symmetry.
An exact proof term for the current goal is IHy v (SNoR_SNoS y Hy v Hv).
Use f_equal.
We will prove - (- u) * v = u * v.
Use transitivity with and (- - u) * v.
Use symmetry.
We will prove (- - u) * v = - (- u) * v.
An exact proof term for the current goal is IHxy (- u) (SNoR_SNoS x Hx (- u) Lmu2) v (SNoR_SNoS y Hy v Hv).
rewrite the current goal using minus_SNo_invol u Hua (from left to right).
Use reflexivity.
rewrite the current goal using L1 (from left to right).
We will prove - ((- u) * y + x * v + - (- u) * v) ∈ {- w|w ∈ L}.
Apply ReplI L (λw ⇒ - w) to the current goal.
We will prove (- u) * y + x * v + - (- u) * v ∈ L.
Apply HLI2 to the current goal.
We will prove - u ∈ SNoR x.
An exact proof term for the current goal is Lmu2.
We will prove v ∈ SNoR y.
An exact proof term for the current goal is Hv.
Let u be given.
Assume Hu: u ∈ SNoR (- x).
Let v be given.
Assume Hv: v ∈ SNoL y.
Apply SNoR_E (- x) Lmx u Hu to the current goal.
Assume Hua: SNo u.
Assume Hub: SNoLev u ∈ SNoLev (- x).
Assume Huc: - x < u.
Apply SNoL_E y Hy v Hv to the current goal.
Assume Hva _ _.
We prove the intermediate claim Lmu1: SNo (- u).
An exact proof term for the current goal is SNo_minus_SNo u Hua.
We prove the intermediate claim Lmu2: - u ∈ SNoL x.
Apply SNoL_I x Hx (- u) Lmu1 to the current goal.
We will prove SNoLev (- u) ∈ SNoLev x.
rewrite the current goal using minus_SNo_Lev u Hua (from left to right).
rewrite the current goal using minus_SNo_Lev x Hx (from right to left).
An exact proof term for the current goal is Hub.
We will prove - u < x.
An exact proof term for the current goal is minus_SNo_Lt_contra1 x u Hx Hua Huc.
We will prove u * y + (- x) * v + - u * v ∈ {- w|w ∈ L}.
We prove the intermediate claim L1: u * y + (- x) * v + - u * v = - ((- u) * y + x * v + - (- u) * v).
Use symmetry.
Use transitivity with and - (- u) * y + - x * v + - - (- u) * v.
An exact proof term for the current goal is minus_add_SNo_distr_3 ((- u) * y) (x * v) (- (- u) * v) (SNo_mul_SNo (- u) y Lmu1 Hy) (SNo_mul_SNo x v Hx Hva) (SNo_minus_SNo ((- u) * v) (SNo_mul_SNo (- u) v Lmu1 Hva)).
Use f_equal.
We will prove - (- u) * y = u * y.
Use transitivity with and (- - u) * y.
Use symmetry.
An exact proof term for the current goal is IHx (- u) (SNoL_SNoS x Hx (- u) Lmu2).
rewrite the current goal using minus_SNo_invol u Hua (from left to right).
Use reflexivity.
Use f_equal.
We will prove - x * v = (- x) * v.
Use symmetry.
An exact proof term for the current goal is IHy v (SNoL_SNoS y Hy v Hv).
Use f_equal.
We will prove - (- u) * v = u * v.
Use transitivity with and (- - u) * v.
Use symmetry.
We will prove (- - u) * v = - (- u) * v.
An exact proof term for the current goal is IHxy (- u) (SNoL_SNoS x Hx (- u) Lmu2) v (SNoL_SNoS y Hy v Hv).
rewrite the current goal using minus_SNo_invol u Hua (from left to right).
Use reflexivity.
rewrite the current goal using L1 (from left to right).
We will prove - ((- u) * y + x * v + - (- u) * v) ∈ {- w|w ∈ L}.
Apply ReplI L (λw ⇒ - w) to the current goal.
We will prove (- u) * y + x * v + - (- u) * v ∈ L.
Apply HLI1 to the current goal.
We will prove - u ∈ SNoL x.
An exact proof term for the current goal is Lmu2.
We will prove v ∈ SNoL y.
An exact proof term for the current goal is Hv.
We will prove {- w|w ∈ L} ⊆ R'.
Let a be given.
Assume Ha.
Apply ReplE_impred L (λw ⇒ - w) a Ha to the current goal.
Let w be given.
Assume Hw: w ∈ L.
Assume Hwe: a = - w.
rewrite the current goal using Hwe (from left to right).
We will prove - w ∈ R'.
Apply HLE w Hw to the current goal.
Let u be given.
Assume Hu: u ∈ SNoL x.
Let v be given.
Assume Hv: v ∈ SNoL y.
Assume Hwuv: w = u * y + x * v + - u * v.
Apply SNoL_E x Hx u Hu to the current goal.
Assume Hua: SNo u.
Assume Hub: SNoLev u ∈ SNoLev x.
Assume Huc: u < x.
Apply SNoL_E y Hy v Hv to the current goal.
Assume Hva _ _.
We prove the intermediate claim Lmu1: SNo (- u).
An exact proof term for the current goal is SNo_minus_SNo u Hua.
We prove the intermediate claim Lmu2: - u ∈ SNoR (- x).
Apply SNoR_I (- x) (SNo_minus_SNo x Hx) (- u) Lmu1 to the current goal.
We will prove SNoLev (- u) ∈ SNoLev (- x).
rewrite the current goal using minus_SNo_Lev u Hua (from left to right).
rewrite the current goal using minus_SNo_Lev x Hx (from left to right).
An exact proof term for the current goal is Hub.
We will prove - x < - u.
An exact proof term for the current goal is minus_SNo_Lt_contra u x Hua Hx Huc.
We prove the intermediate claim L1: - w = (- u) * y + (- x) * v + - (- u) * v.
rewrite the current goal using Hwuv (from left to right).
rewrite the current goal using minus_add_SNo_distr_3 (u * y) (x * v) (- (u * v)) (SNo_mul_SNo u y Hua Hy) (SNo_mul_SNo x v Hx Hva) (SNo_minus_SNo (u * v) (SNo_mul_SNo u v Hua Hva)) (from left to right).
Use f_equal.
We will prove - (u * y) = (- u) * y.
Use symmetry.
An exact proof term for the current goal is IHx u (SNoL_SNoS x Hx u Hu).
Use f_equal.
We will prove - (x * v) = (- x) * v.
Use symmetry.
An exact proof term for the current goal is IHy v (SNoL_SNoS y Hy v Hv).
Use f_equal.
We will prove - (u * v) = (- u) * v.
Use symmetry.
An exact proof term for the current goal is IHxy u (SNoL_SNoS x Hx u Hu) v (SNoL_SNoS y Hy v Hv).
rewrite the current goal using L1 (from left to right).
We will prove (- u) * y + (- x) * v + - (- u) * v ∈ R'.
Apply HR'I2 to the current goal.
An exact proof term for the current goal is Lmu2.
An exact proof term for the current goal is Hv.
Let u be given.
Assume Hu: u ∈ SNoR x.
Let v be given.
Assume Hv: v ∈ SNoR y.
Assume Hwuv: w = u * y + x * v + - u * v.
Apply SNoR_E x Hx u Hu to the current goal.
Assume Hua: SNo u.
Assume Hub: SNoLev u ∈ SNoLev x.
Assume Huc: x < u.
Apply SNoR_E y Hy v Hv to the current goal.
Assume Hva _ _.
We prove the intermediate claim Lmu1: SNo (- u).
An exact proof term for the current goal is SNo_minus_SNo u Hua.
We prove the intermediate claim Lmu2: - u ∈ SNoL (- x).
Apply SNoL_I (- x) (SNo_minus_SNo x Hx) (- u) Lmu1 to the current goal.
We will prove SNoLev (- u) ∈ SNoLev (- x).
rewrite the current goal using minus_SNo_Lev u Hua (from left to right).
rewrite the current goal using minus_SNo_Lev x Hx (from left to right).
An exact proof term for the current goal is Hub.
We will prove - u < - x.
An exact proof term for the current goal is minus_SNo_Lt_contra x u Hx Hua Huc.
We prove the intermediate claim L1: - w = (- u) * y + (- x) * v + - (- u) * v.
rewrite the current goal using Hwuv (from left to right).
rewrite the current goal using minus_add_SNo_distr_3 (u * y) (x * v) (- (u * v)) (SNo_mul_SNo u y Hua Hy) (SNo_mul_SNo x v Hx Hva) (SNo_minus_SNo (u * v) (SNo_mul_SNo u v Hua Hva)) (from left to right).
Use f_equal.
We will prove - (u * y) = (- u) * y.
Use symmetry.
An exact proof term for the current goal is IHx u (SNoR_SNoS x Hx u Hu).
Use f_equal.
We will prove - (x * v) = (- x) * v.
Use symmetry.
An exact proof term for the current goal is IHy v (SNoR_SNoS y Hy v Hv).
Use f_equal.
We will prove - (u * v) = (- u) * v.
Use symmetry.
An exact proof term for the current goal is IHxy u (SNoR_SNoS x Hx u Hu) v (SNoR_SNoS y Hy v Hv).
rewrite the current goal using L1 (from left to right).
We will prove (- u) * y + (- x) * v + - (- u) * v ∈ R'.
Apply HR'I1 to the current goal.
An exact proof term for the current goal is Lmu2.
An exact proof term for the current goal is Hv.
∎