rcases h2 with ⟨lit, ⟨hlit1, hlit2⟩⟩
n : Nat
lratClause : LRAT.DefaultClause n
assign : PosFin n → Bool
clause : Clause (PosFin n)
h : clause.convertLRAT' = some lratClause
h2 : ∃ x, x ∈ clause ∧ (assign x.fst == x.snd) = true
⊢ ∃ x, x ∈ LRAT.Clause.toList lratClause ∧ assign x.fst = x.snd
case intro.intro
n : Nat
lratClause : LRAT.DefaultClause n
assign : PosFin n → Bool
clause : Clause (PosFin n)
h : clause.convertLRAT' = some lratClause
lit : PosFin n × Bool
hlit1 : lit ∈ clause
hlit2 : (assign lit.fst == lit.snd) = true
⊢ ∃ x, x ∈ LRAT.Clause.toList lratClause ∧ assign x.fst = x.snd