Theorem: Prod.Lex.mk_true_lt_iff_lt (Etch/Verification/Misc.lean)

State before:
m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
β : Type ?u.51649
r₁ : α → α → Prop
r₂ : β → β → Prop
inst✝ : PartialOrder α
x : α
y : Lex (α × Bool)
⊢ (x, true) < y ↔ x < y.1
Tactic:
simp [lt_iff']
State after:
no goals