Theorem: ConcatenationTheory.TC3Lang.trivialEnds (ConcatenationTheory/TC3/Preludes.lean)

State before:
τ : Type
inst✝ : TC3Lang τ
x y : τ
⊢ x ⊑ₑ y ⌢ x
Tactic:
exists y
State after:
no goals