Lean4
/-- The core unit-propagation step.
We have a local context of assumptions `¬l'` (sometimes called an assignment)
and we wish to add `¬l` to the context, that is, we want to prove `l` is also falsified.
This is because there is a clause `a ∨ b ∨ ¬l` in the global context
such that all literals in the clause are falsified except for `¬l`;
so in the context `h₁` where we suppose that `¬l` is falsified,
the clause itself is falsified so we can prove `False`.
We continue the proof in `h₂`, with the assumption that `l` is falsified. -/
theorem by_cases {v : Valuation} {l} (h₁ : v.neg l.negate → False) (h₂ : v.neg l → False) : False :=
match l with
| Literal.pos _ => h₂ h₁
| Literal.neg _ => h₁ h₂
