cases c₂:h₂
a c : Answer
h₁ : a ≤ Answer.yes
h₂ : Answer.yes ≤ c
c₁ : h₁ = ⋯
⊢ a ≤ c
case le_yes
a : Answer
h₁ : a ≤ Answer.yes
c₁ : h₁ = ⋯
h₂ : Answer.yes ≤ Answer.yes
c₂ : h₂ = ⋯
⊢ a ≤ Answer.yes

case refl
a : Answer
h₁ : a ≤ Answer.yes
c₁ : h₁ = ⋯
h₂ : Answer.yes ≤ Answer.yes
c₂ : h₂ = ⋯
⊢ a ≤ Answer.yes