English
IH24 remains valid under negation: applying negation to all arguments yields equality of two IH24 statements with negated inputs.
Русский
IH24 сохраняется при отрицании: применение отрицания ко всем аргументам даёт равенство двух IH24 с отрицательными входами.
LaTeX
$$IH24 x1 x2 y → IH24 (-x2) (-x1) y ∧ IH24 x1 x2 (-y)$$
Lean4
theorem ih4 (ih' : ∀ a, ArgsRel a (Args.P24 x₁ x₂ y) → P124 a) : IH4 x₁ x₂ y :=
by
refine fun z w h ↦ ⟨?_, ?_⟩
all_goals
intro h'
apply
(ih' (Args.P24 _ _ _) <| (TransGen.single _).tail <| (cutExpand_add_left { x₁ }).2 <| cutExpand_pair_right h).1
try exact (cutExpand_add_right { w }).2 <| cutExpand_pair_left h'
try exact (cutExpand_add_right { w }).2 <| cutExpand_pair_right h'
