Theorem: LeanSAT.ILit.exists_succ_toVar (LeanSAT/Data/ICnf.lean)

State before:
l : ILit
⊢ ∃ n, ↑(toVar l) = n + 1
Tactic:
exact Nat.exists_eq_add_of_le' (toVar l).property
State after:
no goals