α✝ : Type ?u.81083
β : Type ?u.81086
γ✝ : Type ?u.81089
δ : Type ?u.81092
r✝ : α✝ → α✝ → Prop
s✝ : β → β → Prop
t✝ : γ✝ → γ✝ → Prop
u : δ → δ → Prop
α γ : Type u
r : α → α → Prop
t : γ → γ → Prop
x : α
s : α → α → Prop
h₁' : α = γ
h₂ : HEq r s
h₂' : HEq s t
⊢ ↑(RelIso.trans (RelIso.cast (_ : α = α) h₂) (RelIso.cast h₁' h₂')) x = ↑(RelIso.cast (_ : α = γ) (_ : HEq r t)) x
α✝ : Type ?u.81083
β✝ : Type ?u.81086
γ✝ : Type ?u.81089
δ : Type ?u.81092
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
u : δ → δ → Prop
α β γ : Type u
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
h₁ : α = β
h₁' : β = γ
h₂ : HEq r s
h₂' : HEq s t
x : α
⊢ ↑(RelIso.trans (RelIso.cast h₁ h₂) (RelIso.cast h₁' h₂')) x = ↑(RelIso.cast (_ : α = γ) (_ : HEq r t)) x
subst h₁
no goals
α✝ : Type ?u.81083
β : Type ?u.81086
γ✝ : Type ?u.81089
δ : Type ?u.81092
r✝ : α✝ → α✝ → Prop
s✝ : β → β → Prop
t✝ : γ✝ → γ✝ → Prop
u : δ → δ → Prop
α γ : Type u
r : α → α → Prop
t : γ → γ → Prop
x : α
s : α → α → Prop
h₁' : α = γ
h₂ : HEq r s
h₂' : HEq s t
⊢ ↑(RelIso.trans (RelIso.cast (_ : α = α) h₂) (RelIso.cast h₁' h₂')) x = ↑(RelIso.cast (_ : α = γ) (_ : HEq r t)) x
rfl