Let L = L'U {l}. By the induction hypothesis, we can assume that ForgetLit(E, L') is the most general consequence of Σ that is Lit-independent from L ′ . For the sake of simplicity, let Σ′ denote this formula.  It remains to show that ForgetLit(Σ,L) =
ForgetLit(ForgetLit(Σ, L′), {l}) = ForgetLit(Σ′, {l}) is the most general consequence of E' that is Lit-independent from l. Two cases are to be considered:
- l = x . ForgetLit( ) is Lit-independent from x if and only if ForgetLit(Σ′, x) = ForgetLit(Σ′, x) x← 0 holds. We have

$$\vee\Sigma_{x\leftarrow}^{\prime}$$

()),(1 V (-x A )),(-o = (),(-1 V ),(-o)
This formula clearly is a logical consequence of For getLit(Σ ′ , { x }). Hence For getLit(Σ ′ , x )
is Lit-independent from x . ForgetLit( Σ ′ x ) is a logical consequence of Σ ′ . Indeed, for every ∑ ′ ∈ PROP PS , x ∈ PS , we have ∑ ′ ≡ ( x ∧ ∑ ′ x √ 1 ) ∨ (¬ x ∧ ∑ ′ x √ n ). It remains to show that every logical consequence Φ of Σ ′ that is Lit-independent from x is a logical consequence of ForgetLit( ) ′ , x ). Let Φ any formula s.t. Σ ′ |= Φ holds and Φ |= Φ x ← 0 .  Since Σ ′ ≡ ( x ∧ Σ ′ x ← 1 ) ∨ ( − x ∧ Σ ′ x ← 0 ) holds, we have Σ ′ |= Φ if and only if both (x A E r ← 1 ) |= Φ and (¬ x A Σ ′ x ← 0 ) |= Φ hold. Thus, in order to show that ForgetLit(Σ′, x) |= Φ holds, it is sufficient to prove that Σ′, ← 1 |= Φ holds. Suppose that is not the case. Then, there exists an implicant γ of Σ x ← 1 that is not an implicant of Φ  However, since ( x ∧ Σ t ← 1 ) |= Φ holds, we know that ( x ∧ γ ) is an implicant of Φ. Since Φ is equivalent to the conjunction of its prime implicates, there necessarily exists a prime implicate π of Φ s.t. ( x ∧ γ ) |= π and γ | ̸= π hold. This imposes that x belongs to π but no literal of γ belongs to π . By construction, π x ← 0 is an implicate of Qx~o and 7r~o is strictly stronger than 7r. Since Q E Qx~o holds, Q E 7r~o holds as well. This contradicts the fact that π is a prime implicate of Φ .

- l = -x. The demonstration is similar, mutatis mutandis.

Proposition 17   Let Σ, Φ be two formulas from PROPps and L ⊆ Lps.

ForgetLit(Σ V Φ, L) ≡ ForgetLit(Σ, L) V ForgetLit(Φ, L).

Proof:  The claim can be easily proved from Proposition 15.  Indeed, the models of ForgetLit(Σ VΦ, L ) are the models ω such that Force(ω, L 1 ) |= Σ VΦ, where L 1 ⊆ L . Now, Force(ω, L 1 ) |= Σ V Φ holds if and only if Force(ω, L 1 ) |= Σ holds or Force(ω, L 1 ) |= Φ
holds.

On the other hand, the models of ForgetLit(E, L) V ForgetLit(Φ, L) are those such that Force(ω, L 1 ) |= Σ or Force(ω, L 1 ) |= Φ for some L 1 ⊆ L . This is equivalent to the above condition.