case mk
α : Type ?u.19042
β : Type ?u.19045
γ : Type ?u.19048
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
α✝ : Type u_1
r✝ : α✝ → α✝ → Prop
wo✝ : IsWellOrder α✝ r✝
⊢ { α := { α := α✝, r := r✝, wo := wo✝ }.α, r := { α := α✝, r := r✝, wo := wo✝ }.r,
      wo := (_ : IsWellOrder { α := α✝, r := r✝, wo := wo✝ }.α { α := α✝, r := r✝, wo := wo✝ }.r) } =
    { α := α✝, r := r✝, wo := wo✝ }
α : Type ?u.19042
β : Type ?u.19045
γ : Type ?u.19048
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : WellOrder
⊢ { α := o.α, r := o.r, wo := (_ : IsWellOrder o.α o.r) } = o
cases o
no goals
case mk
α : Type ?u.19042
β : Type ?u.19045
γ : Type ?u.19048
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
α✝ : Type u_1
r✝ : α✝ → α✝ → Prop
wo✝ : IsWellOrder α✝ r✝
⊢ { α := { α := α✝, r := r✝, wo := wo✝ }.α, r := { α := α✝, r := r✝, wo := wo✝ }.r,
      wo := (_ : IsWellOrder { α := α✝, r := r✝, wo := wo✝ }.α { α := α✝, r := r✝, wo := wo✝ }.r) } =
    { α := α✝, r := r✝, wo := wo✝ }
rfl