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

State before:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
γ : Type
decl : Decl α
g : α → β
h : β → γ
⊢ relabel (h ∘ g) decl = relabel h (relabel g decl)
Tactic:
cases decl <;> rfl
State after:
no goals