apply hconst
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
aig : AIG α
hstart : start < aig.decls.size
prop : Prop
hconst : ∀ (b : Bool), aig.decls[start] = Decl.const b → prop
hatom : ∀ (a : α), aig.decls[start] = Decl.atom a → prop
hgate : ∀ (lhs rhs : Nat) (linv rinv : Bool), aig.decls[start] = Decl.gate lhs rhs linv rinv → prop
b : Bool
h : aig.decls[start] = Decl.const b
⊢ prop
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
aig : AIG α
hstart : start < aig.decls.size
prop : Prop
hconst : ∀ (b : Bool), aig.decls[start] = Decl.const b → prop
hatom : ∀ (a : α), aig.decls[start] = Decl.atom a → prop
hgate : ∀ (lhs rhs : Nat) (linv rinv : Bool), aig.decls[start] = Decl.gate lhs rhs linv rinv → prop
b : Bool
h : aig.decls[start] = Decl.const b
⊢ aig.decls[start] = Decl.const ?b

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