Theorem: Decl.relabel_id_map (LeanSAT/AIG/Relabel.lean)

State before:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
decl : Decl α
⊢ relabel id decl = decl
Tactic:
simp only [relabel, id_eq]
State after:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
decl : Decl α
⊢ (match decl with
    | const b => const b
    | atom a => atom a
    | gate lhs rhs linv rinv => gate lhs rhs linv rinv) =
    decl

State before:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
decl : Decl α
⊢ (match decl with
    | const b => const b
    | atom a => atom a
    | gate lhs rhs linv rinv => gate lhs rhs linv rinv) =
    decl
Tactic:
cases decl <;> rfl
State after:
no goals