cases g <;> simp [ofBoolExprCached.go, Gate.eval, lih, rih]
case gate
assign : BVExpr.Assignment
g : Gate
lhs rhs : BoolExpr BVPred
lih : ∀ (aig : AIG BVBit), ⟦(ofBoolExprCached.go lhs aig BVPred.bitblast).val, assign.toAIGAssignment⟧ = eval assign lhs
rih : ∀ (aig : AIG BVBit), ⟦(ofBoolExprCached.go rhs aig BVPred.bitblast).val, assign.toAIGAssignment⟧ = eval assign rhs
aig : AIG BVBit
⊢ ⟦(ofBoolExprCached.go (BoolExpr.gate g lhs rhs) aig BVPred.bitblast).val, assign.toAIGAssignment⟧ =
    eval assign (BoolExpr.gate g lhs rhs)
no goals