apply idx_trichotomy aig hstart
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
res : Bool
aig : AIG α
hstart : start < aig.decls.size
hconst :
  ∀ (b : Bool),
    aig.decls[start] = Decl.const b → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hatom :
  ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hgate :
  ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
⊢ ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
case hconst
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
res : Bool
aig : AIG α
hstart : start < aig.decls.size
hconst :
  ∀ (b : Bool),
    aig.decls[start] = Decl.const b → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hatom :
  ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hgate :
  ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
⊢ ∀ (b : Bool),
    aig.decls[start] = Decl.const b → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res

case hatom
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
res : Bool
aig : AIG α
hstart : start < aig.decls.size
hconst :
  ∀ (b : Bool),
    aig.decls[start] = Decl.const b → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hatom :
  ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hgate :
  ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
⊢ ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res

case hgate
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
res : Bool
aig : AIG α
hstart : start < aig.decls.size
hconst :
  ∀ (b : Bool),
    aig.decls[start] = Decl.const b → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hatom :
  ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hgate :
  ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
⊢ ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res