What exactly is "large elimination"?
You are incorrect about the definition of large elimination: it refers to the ability to build values of type $\mathrm{Type}$ by eliminating an inductive value. The canonical example:

bool_to_type : bool -&gt; Type := fun b =&gt;
     match b with
         | true =&gt; Unit
         | false =&gt; Empty


Where Unit and Empty are inductive types with 1 and 0 constructors, respectively. Notably, this allows you to prove the proposition $0 \not= 1$, which cannot be proven without this ability.

As noted in another answer (https://cstheory.stackexchange.com/a/21878/3984) a good resource that explains this is the following github repo: https://github.com/FStarLang/FStar/issues/360