apply w
x : BoolExpr Nat
f g : Nat → Bool
i : Nat
w : ∀ (i_1 : Nat), i_1 < (literal i).vars → f i_1 = g i_1
⊢ f i = g i
case a
x : BoolExpr Nat
f g : Nat → Bool
i : Nat
w : ∀ (i_1 : Nat), i_1 < (literal i).vars → f i_1 = g i_1
⊢ i < (literal i).vars