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