Theorem: AIG.toCNF.satAssignment_inr (LeanSAT/AIG/CNF.lean)

State before:
aig : AIG Nat
assign1 : Nat → Bool
x : Fin aig.decls.size
⊢ cnfSatAssignment aig assign1 (Sum.inr x) = ⟦{ aig := aig, ref := { gate := ↑x, hgate := ⋯ } }, assign1⟧
Tactic:
simp [cnfSatAssignment, mixAssigns]
State after:
no goals