unfold denote denote.go
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
⊢ ⟦aig.mkConst val, assign⟧ = val
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
⊢ (match elem : (aig.mkConst val).aig.decls[(aig.mkConst val).ref.gate] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := denote.go lhs (aig.mkConst val).aig.decls assign ⋯ ⋯;
      let rval := denote.go rhs (aig.mkConst val).aig.decls assign ⋯ ⋯;
      xor lval linv && xor rval rinv) =
    val