contradiction
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : (aig.mkConst val).aig.decls[(aig.mkConst val).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq : Decl.const val = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := denote.go lidx✝ (aig.mkConst val).aig.decls assign ⋯ ⋯;
    let rval := denote.go ridx✝ (aig.mkConst val).aig.decls assign ⋯ ⋯;
    xor lval linv✝ && xor rval rinv✝) =
    val
no goals