Context complete

theorem Context.complete (p : Process Name Constant) :    ∃ c : Context Name Constant, p = c<[(Process.nil : Process Name Constant)] ∨    ∃ k : Constant, p = c<[(Process.const k : Process Name Constant)] := by  induction p  case nil =>    exists hole    grind  case pre μ p ih =>    obtain ⟨c, hc⟩ := ih    exists pre μ c    grind  case par p q ihp ihq =>    obtain ⟨cp, hcp⟩ := ihp    exists parL cp q    grind  case choice p q ihp ihq =>    obtain ⟨cp, hcp⟩ := ihp    exists choiceL cp q    grind  case res a p ih =>    obtain ⟨c, hc⟩ := ih    exists res a c    grind  case const k =>    exists hole    grind