simp only [Function.comp_apply, relabel, List.map_map]
case h
α✝² α✝¹ : Type
f : α✝² → α✝¹
α✝ : Type
g : α✝ → α✝²
i : Clause α✝
⊢ (relabel f ∘ relabel g) i = relabel (f ∘ g) i
case h
α✝² α✝¹ : Type
f : α✝² → α✝¹
α✝ : Type
g : α✝ → α✝²
i : Clause α✝
⊢ List.map ((fun x => (f x.fst, x.snd)) ∘ fun x => (g x.fst, x.snd)) i = List.map (fun x => (f (g x.fst), x.snd)) i