∀ {cont : Type u_1} {idx : Type u_2} {elem : Type u_3} {dom : cont → idx → Prop} [inst : GetElem? cont idx elem dom]
  [LawfulGetElem cont idx elem dom] {c : cont} {i : idx} [Decidable (dom c i)] (h : dom c i), c[i]? = some c[i] ↔ True