case disj =>
  intro a b h a' b' h₁ h₂
  match a', b', h₁, h₂ with | _, _, .head _, .head _ => ?_
  exact h
axs : Statement → Prop
ax : Statement
H : axs ax
⊢ DJ.subst VR.expr ax.ctx.dj ax.ctx.dj
no goals