let rec mk_inj i a = if i <= 0 then mk_inl a else if i = 1 then mk_inr a else mk_inr (mk_inj (i - 1) a)