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

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