simp [CNF.sat, denote_idx_gate heq]
upper lhs rhs : Nat
linv rinv : Bool
aig : AIG Nat
h : upper < aig.decls.size
heq : aig.decls[upper] = Decl.gate lhs rhs linv rinv
assign1 : Nat → Bool
⊢ (Decl.gateToCNF (Sum.inr ⟨upper, h⟩) (Sum.inr ⟨lhs, ⋯⟩) (Sum.inr ⟨rhs, ⋯⟩) linv rinv).sat
    (cnfSatAssignment aig assign1)
no goals