simp [CNF.sat, denote_idx_const heq]
upper : Nat
aig : AIG Nat
h : upper < aig.decls.size
b : Bool
heq : aig.decls[upper] = Decl.const b
assign1 : Nat → Bool
⊢ (Decl.constToCNF (Sum.inr ⟨upper, h⟩) b).sat (cnfSatAssignment aig assign1)
no goals