Theorem: MotivatedTree.funext_ord (MotivatedMoves/Moves/TreeRewriteOrd.lean)

State before:
α : Type u
β : Type v
inst✝ : Preorder β
f g : α → β
h : ∀ (a : α), f a ≤ g a
⊢ f ≤ g
Tactic:
exact h
State after:
no goals