simp [CNF.sat, denote_idx_atom heq]
upper : Nat
aig : AIG Nat
h : upper < aig.decls.size
a : Nat
heq : aig.decls[upper] = Decl.atom a
assign1 : Nat → Bool
⊢ (Decl.atomToCNF (Sum.inr ⟨upper, h⟩) (Sum.inl a)).sat (cnfSatAssignment aig assign1)
no goals