α : Type ?u.341106
β : Type ?u.341109
γ : Type ?u.341112
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
h : (lsub fun i => typein (fun x x_1 => x < x_1) i) < o
⊢ False
α : Type ?u.341106
β : Type ?u.341109
γ : Type ?u.341112
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
⊢ o ≤ lsub fun i => typein (fun x x_1 => x < x_1) i
by_contra' h
α : Type ?u.341106
β : Type ?u.341109
γ : Type ?u.341112
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
h : (lsub fun i => typein (fun x x_1 => x < x_1) i) < type fun x x_1 => x < x_1
⊢ False
α : Type ?u.341106
β : Type ?u.341109
γ : Type ?u.341112
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
h : (lsub fun i => typein (fun x x_1 => x < x_1) i) < o
⊢ False
conv_rhs at h => rw [← type_lt o]